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