Metamath Proof Explorer

Theorem dfac2

Description: Axiom of Choice (first form) of Enderton p. 49 corresponds to our Axiom of Choice (in the form of ac3 ). The proof does not make use of AC, but the Axiom of Regularity is used (by applying dfac2b ). (Contributed by NM, 5-Apr-2004) (Revised by Mario Carneiro, 26-Jun-2015) (Revised by AV, 16-Jun-2022)

Ref Expression
Assertion dfac2 ⊢ CHOICE ↔ ∀ x ∃ y ∀ z ∈ x z ≠ ∅ → ∃! w ∈ z ∃ v ∈ y z ∈ v ∧ w ∈ v

Proof

Step Hyp Ref Expression
1 dfac2b ⊢ CHOICE → ∀ x ∃ y ∀ z ∈ x z ≠ ∅ → ∃! w ∈ z ∃ v ∈ y z ∈ v ∧ w ∈ v
2 dfac2a ⊢ ∀ x ∃ y ∀ z ∈ x z ≠ ∅ → ∃! w ∈ z ∃ v ∈ y z ∈ v ∧ w ∈ v → CHOICE
3 1 2 impbii ⊢ CHOICE ↔ ∀ x ∃ y ∀ z ∈ x z ≠ ∅ → ∃! w ∈ z ∃ v ∈ y z ∈ v ∧ w ∈ v