Metamath Proof Explorer


Theorem axpowndlem1

Description: Lemma for the Axiom of Power Sets with no distinct variable conditions. (Contributed by NM, 4-Jan-2002)

Ref Expression
Assertion axpowndlem1 x x = y ¬ x = y x y x z x y y x z y x

Proof

Step Hyp Ref Expression
1 pm2.24 x = y ¬ x = y x y x z x y y x z y x
2 1 sps x x = y ¬ x = y x y x z x y y x z y x