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