Using the replacements I gave above yielded the proof:
${
$d z A $. $d x y z $. $d z ph $.
sbcex2f.1 $e |- F/_ x A $.
$( Move existential quantifier in and out of class substitution.
(Contributed by NM, 21-May-2004.) (Revised by NM, 18-Aug-2018.) $)
sbcex2f $p |- ( [. A / y ]. E. x ph <-> E. x [. A / y ]. ph ) $=
( vz wex wsbc cvv wcel sbcex nfel1 exlimi wsb dfsbcq2 nfeq2
exbid
cv wceq sbex vtoclbg pm5.21nii )
ABGZCDHZDIJZACDHZBGZUCCDKUFUEBBD
IELACDKMUCCFNACFNZBGUDUGFDIUCCFDOFRZDSUHUFBBUIDEPACFDOQABCFTUAUB
$.
$}
The technique is the following. Suppose you have |- T[x, A] where $d x A,
> and you wish to prove |- F/_ x A => |- T[x, A]. You apply the theorem
> substituting y for x and A for A, where y is a new dummy variable, so that
> $d y A is satisfied. You obtain |- T[y, A], and apply chvar to obtain |-
> T[x, A] (or just use mpbir if T[x, A] binds x). The side goal is |- ( x = y
> -> ( T[y, A] <-> T[x, A] ) ), where you can use equality theorems, except
> that when you get to a bound variable you use a non-dv bound variable
> renamer theorem like cbval. The section
> us2.metamath.org/mpeuni/mmtheorems32.html#mm3146s also describes the
> metatheorem that underlies this.
>
That's a nice general technique. It is illustrated by a proof from today!
Look at the proof of mo2 from mo2v; it uses cbvex.
--
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 [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/78ff1831-a446-48fc-9599-01bf43051ae2%40googlegroups.com.
