Metamath Proof Explorer

Theorem dfac0

Description: Equivalence of two versions of the Axiom of Choice. The proof uses the Axiom of Regularity. The right-hand side is our original ax-ac . (Contributed by Mario Carneiro, 17-May-2015)

Ref Expression
Assertion dfac0 ⊢CHOICE↔∀x∃y∀z∀wz∈w∧w∈x→∃v∀u∃tu∈w∧w∈t∧u∈t∧t∈y↔u=v

Proof

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