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

Metamath Proof Explorer

Theorem axacndlem3

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 axacndlem3 ⊢ ∀ y y = 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 ⊢ Ⅎ z ∀ y y = z
2 simpl ⊢ y ∈ z ∧ z ∈ w → y ∈ z
3 2 alimi ⊢ ∀ x y ∈ z ∧ z ∈ w → ∀ x y ∈ z
4 nd3 ⊢ ∀ y y = z → ¬ ∀ x y ∈ z
5 4 pm2.21d ⊢ ∀ y y = z → ∀ x y ∈ z → ∃ w ∀ y ∃ w y ∈ z ∧ z ∈ w ∧ y ∈ w ∧ w ∈ x ↔ y = w
6 3 5 syl5 ⊢ ∀ y y = z → ∀ x y ∈ z ∧ z ∈ w → ∃ w ∀ y ∃ w y ∈ z ∧ z ∈ w ∧ y ∈ w ∧ w ∈ x ↔ y = w
7 1 6 alrimi ⊢ ∀ y y = z → ∀ z ∀ x y ∈ z ∧ z ∈ w → ∃ w ∀ y ∃ w y ∈ z ∧ z ∈ w ∧ y ∈ w ∧ w ∈ x ↔ y = w
8 7 axc4i ⊢ ∀ y y = z → ∀ y ∀ z ∀ x y ∈ z ∧ z ∈ w → ∃ w ∀ y ∃ w y ∈ z ∧ z ∈ w ∧ y ∈ w ∧ w ∈ x ↔ y = w
9 8 19.8ad ⊢ ∀ y y = z → ∃ x ∀ y ∀ z ∀ x y ∈ z ∧ z ∈ w → ∃ w ∀ y ∃ w y ∈ z ∧ z ∈ w ∧ y ∈ w ∧ w ∈ x ↔ y = w