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 ⊢∀xx=y→∃x∀y∀z∀xy∈z∧z∈w→∃w∀y∃wy∈z∧z∈w∧y∈w∧w∈x↔y=w

Proof

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