Metamath Proof Explorer

Theorem axacndlem2

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 axacndlem2 ⊢ ∀ x x = z → ∃ 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 = z
2 nfae ⊢ Ⅎ z ∀ x x = z
3 simpr ⊢ y ∈ z ∧ z ∈ w → z ∈ w
4 3 alimi ⊢ ∀ x y ∈ z ∧ z ∈ w → ∀ x z ∈ w
5 nd1 ⊢ ∀ x x = z → ¬ ∀ x z ∈ w
6 5 pm2.21d ⊢ ∀ x x = z → ∀ x z ∈ w → ∃ w ∀ y ∃ w y ∈ z ∧ z ∈ w ∧ y ∈ w ∧ w ∈ x ↔ y = w
7 4 6 syl5 ⊢ ∀ x x = z → ∀ x y ∈ z ∧ z ∈ w → ∃ w ∀ y ∃ w y ∈ z ∧ z ∈ w ∧ y ∈ w ∧ w ∈ x ↔ y = w
8 2 7 alrimi ⊢ ∀ x x = z → ∀ 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 = z → ∀ 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 = z → ∃ x ∀ y ∀ z ∀ x y ∈ z ∧ z ∈ w → ∃ w ∀ y ∃ w y ∈ z ∧ z ∈ w ∧ y ∈ w ∧ w ∈ x ↔ y = w