On Thu, Oct 12, 2023 at 1:46 AM bil...@gmail.com <bill...@gmail.com> wrote:
> I am at a more basic level than what you are trying to address. My goal is
> to learn how to prove theorems in metamath.
>
> My current task is to do the follow: given B = { x | ph }, how would I
> prove that A e. B. This is beginning level stuff.
>
> I see that there is theorem elab2g that would be useful: I just need to
> show the following: x = A -> ( ph <-> ps )
>
Yes that's the right theorem to apply when this is your goal. Normally you
would take ps to be ph with all occurrences of x replaced by A, and use
equality theorems to prove it.
> For substitution: df-sb: [t/x] phi <-> Ay ( y = t -> Ax ( x = y -> phi ))
> I find this more intuitive: sb5 |- ( [. y / x ]. ph <-> E. x ( x = y /\
> ph )
>
Generally you should not need to deal with the definitions of basic
functions like this (in fact, even in advanced definitions you almost never
use the definition directly, you prove an extraction lemma and use the
lemma instead of the definition). It is defined in a slightly weird way to
deal with some edge cases involving when t is x or an expression containing
x, but generally you can just choose it to not overlap and then the
definition simplifies. The usual way to unpack a substitution is using sbie
or one of its many variants (such as sbcied2 which shows up in the ismgm
theorem you referenced).
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to metamath+unsubscr...@googlegroups.com.
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/CAFXXJSsrWRicern6Da0%2BXCKM8EpeTbGqL5GNJxe83kNQVqxOrQ%40mail.gmail.com.
