This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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