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

Metamath Proof Explorer

Theorem axacndlem1

Description: Lemma for the Axiom of Choice with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 3-Jan-2002) (New usage is discouraged.)

Ref Expression
Assertion axacndlem1 ⊢ ∀ x x = y → ∃ x ∀ y ∀ z ∀ x y ∈ z ∧ z ∈ w → ∃ w ∀ y ∃ w y ∈ z ∧ z ∈ w ∧ y ∈ w ∧ w ∈ x ↔ y = w

Proof

Step Hyp Ref Expression
1 nfae ⊢ Ⅎ y ∀ x x = y
2 nfae ⊢ Ⅎ z ∀ x x = y
3 simpl ⊢ y ∈ z ∧ z ∈ w → y ∈ z
4 3 alimi ⊢ ∀ x y ∈ z ∧ z ∈ w → ∀ x y ∈ z
5 nd1 ⊢ ∀ x x = y → ¬ ∀ x y ∈ z
6 5 pm2.21d ⊢ ∀ x x = y → ∀ x y ∈ z → ∃ w ∀ y ∃ w y ∈ z ∧ z ∈ w ∧ y ∈ w ∧ w ∈ x ↔ y = w
7 4 6 syl5 ⊢ ∀ x x = y → ∀ x y ∈ z ∧ z ∈ w → ∃ w ∀ y ∃ w y ∈ z ∧ z ∈ w ∧ y ∈ w ∧ w ∈ x ↔ y = w
8 2 7 alrimi ⊢ ∀ x x = y → ∀ z ∀ x y ∈ z ∧ z ∈ w → ∃ w ∀ y ∃ w y ∈ z ∧ z ∈ w ∧ y ∈ w ∧ w ∈ x ↔ y = w
9 1 8 alrimi ⊢ ∀ x x = y → ∀ y ∀ z ∀ x y ∈ z ∧ z ∈ w → ∃ w ∀ y ∃ w y ∈ z ∧ z ∈ w ∧ y ∈ w ∧ w ∈ x ↔ y = w
10 9 19.8ad ⊢ ∀ x x = y → ∃ x ∀ y ∀ z ∀ x y ∈ z ∧ z ∈ w → ∃ w ∀ y ∃ w y ∈ z ∧ z ∈ w ∧ y ∈ w ∧ w ∈ x ↔ y = w