Metamath Proof Explorer

Theorem ac2

Description: Axiom of Choice equivalent. By using restricted quantifiers, we can express the Axiom of Choice with a single explicit conjunction. (If you want to figure it out, the rewritten equivalent ac3 is easier to understand.) Note: aceq0 shows the logical equivalence to ax-ac . (New usage is discouraged.) (Contributed by NM, 18-Jul-1996)

Ref Expression
Assertion ac2 ⊢ ∃ y ∀ z ∈ x ∀ w ∈ z ∃! v ∈ z ∃ u ∈ y z ∈ u ∧ v ∈ u

Proof

Step Hyp Ref Expression
1 ax-ac ⊢ ∃ y ∀ z ∀ w z ∈ w ∧ w ∈ x → ∃ v ∀ u ∃ t u ∈ w ∧ w ∈ t ∧ u ∈ t ∧ t ∈ y ↔ u = v
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 1 2 mpbir ⊢ ∃ y ∀ z ∈ x ∀ w ∈ z ∃! v ∈ z ∃ u ∈ y z ∈ u ∧ v ∈ u