How to instantiate a theorem by substituting a wff in it?

[Philip B.]

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.

[Mario Carneiro]

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

--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/944b447d-0075-4042-91c1-3703ec7635fcn%40googlegroups.com.