If you proved |- ( ph -> E. z ( ps -> ph ) ) in a separate theorem, you could apply it there. If you proved it inline (while proving axext2), then you have to do the substitution manually; I usually do a find and replace of "ph" -> "x = y" and "ps" -> "( z e. x <-> z e. y )" in the part of the proof that was working with "ph" and "ps" to prove that. You can also find and replace "ph" -> "&W1" and "ps" -> "&W2", which means that we use metavariables, which will then be unified with the expressions x = y and ( z e. x <-> z e. y ) in step 500. Mmj2 will not substitute for "ph" and "ps" because in a theorem these are just regular variables (arbitrary but fixed propositions from the context) rather than metavariables (terms awaiting a substitution). Another way to unsubstitute everything is to delete all the formulas in your subproof but keep the left side with the step:hyp:ref; when you run mmj2 on that it will regenerate the formulas with the most general unifier of all those steps, which should clear out ph and ps so that they can be substituted.
Mario On Mon, Feb 1, 2021 at 1:31 AM Philip B. <[email protected]> wrote: > > Hi. I am a metamath newbie playing with mmj2. I am trying to prove axext2 > which is stated as > > qed:: |- E. z ( ( z e. x <-> z e. y ) -> x = y ) > > and to do that, I want to prove separately > > 500:: |- ( x = y -> E. z ( ( z e. x <-> z e. y ) -> x = y ) ) > > and > > 1000:: |- ( -. x = y -> E. z ( ( z e. x <-> z e. y ) -> x = y ) ) > > However, I have a problem even with the *500*. I've proved > > |- ( ph -> E. z ( ps -> ph ) ) > > but I can't figure out how to substitute *x = y* for *ph* and *( z e. x > <-> z e. y )* for *ps* to get *500*. > > -- > 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/944b447d-0075-4042-91c1-3703ec7635fcn%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/944b447d-0075-4042-91c1-3703ec7635fcn%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/CAFXXJSu%3DNocFjfEEHkisQRQT%2Bxwv7d7ud_Hsko1-QM%2BOD%3DG3UQ%40mail.gmail.com.
