Metamath Proof Explorer

Theorem dfac7

Description: Equivalence of the Axiom of Choice (first form) of Enderton p. 49 and our Axiom of Choice (in the form of ac2 ). The proof does not depend on AC but does depend on the Axiom of Regularity. (Contributed by Mario Carneiro, 17-May-2015)

Ref Expression
Assertion dfac7 ⊢ CHOICE ↔ ∀ x ∃ y ∀ z ∈ x ∀ w ∈ z ∃! v ∈ z ∃ u ∈ y z ∈ u ∧ v ∈ u

Proof

Step Hyp Ref Expression
1 dfac2 ⊢ CHOICE ↔ ∀ x ∃ y ∀ z ∈ x z ≠ ∅ → ∃! w ∈ z ∃ v ∈ y z ∈ v ∧ w ∈ v
2 aceq2 ⊢ ∃ y ∀ z ∈ x ∀ w ∈ z ∃! v ∈ z ∃ u ∈ y z ∈ u ∧ v ∈ u ↔ ∃ y ∀ z ∈ x z ≠ ∅ → ∃! w ∈ z ∃ v ∈ y z ∈ v ∧ w ∈ v
3 2 albii ⊢ ∀ x ∃ y ∀ z ∈ x ∀ w ∈ z ∃! v ∈ z ∃ u ∈ y z ∈ u ∧ v ∈ u ↔ ∀ x ∃ y ∀ z ∈ x z ≠ ∅ → ∃! w ∈ z ∃ v ∈ y z ∈ v ∧ w ∈ v
4 1 3 bitr4i ⊢ CHOICE ↔ ∀ x ∃ y ∀ z ∈ x ∀ w ∈ z ∃! v ∈ z ∃ u ∈ y z ∈ u ∧ v ∈ u