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 ∀ w z ∈ w ∧ w ∈ x → ∃ x ∀ z ∃ x z ∈ 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 ∈ y z ∈ u ∧ v ∈ u
2 aceq1 ⊢ ∃ y ∀ z ∈ x ∀ w ∈ z ∃! v ∈ z ∃ u ∈ y z ∈ u ∧ v ∈ u ↔ ∃ y ∀ z ∀ w z ∈ w ∧ w ∈ x → ∃ x ∀ z ∃ x z ∈ w ∧ w ∈ x ∧ z ∈ x ∧ x ∈ y ↔ z = x
3 2 albii ⊢ ∀ x ∃ y ∀ z ∈ x ∀ w ∈ z ∃! v ∈ z ∃ u ∈ y z ∈ u ∧ v ∈ u ↔ ∀ x ∃ y ∀ z ∀ w z ∈ w ∧ w ∈ x → ∃ x ∀ z ∃ x z ∈ w ∧ w ∈ x ∧ z ∈ x ∧ x ∈ y ↔ z = x
4 1 3 bitri ⊢ CHOICE ↔ ∀ x ∃ y ∀ z ∀ w z ∈ w ∧ w ∈ x → ∃ x ∀ z ∃ x z ∈ w ∧ w ∈ x ∧ z ∈ x ∧ x ∈ y ↔ z = x