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.
