Metamath Proof Explorer

Theorem dfac1

Description: Equivalence of two versions of the Axiom of Choice ax-ac . The proof uses the Axiom of Regularity. The right-hand side expresses our AC with the fewest number of different variables. (Contributed by Mario Carneiro, 17-May-2015)

Ref Expression
Assertion dfac1 ⊢CHOICE↔∀x∃y∀z∀wz∈w∧w∈x→∃x∀z∃xz∈w∧w∈x∧z∈x∧x∈y↔z=x

Proof

Step Hyp Ref Expression
1 dfac7 ⊢CHOICE↔∀x∃y∀z∈x∀w∈z∃!v∈z∃u∈yz∈u∧v∈u
2 aceq1 ⊢∃y∀z∈x∀w∈z∃!v∈z∃u∈yz∈u∧v∈u↔∃y∀z∀wz∈w∧w∈x→∃x∀z∃xz∈w∧w∈x∧z∈x∧x∈y↔z=x
3 2 albii ⊢∀x∃y∀z∈x∀w∈z∃!v∈z∃u∈yz∈u∧v∈u↔∀x∃y∀z∀wz∈w∧w∈x→∃x∀z∃xz∈w∧w∈x∧z∈x∧x∈y↔z=x
4 1 3 bitri ⊢CHOICE↔∀x∃y∀z∀wz∈w∧w∈x→∃x∀z∃xz∈w∧w∈x∧z∈x∧x∈y↔z=x