Metamath Proof Explorer

Theorem axac3

Description: This theorem asserts that the constant CHOICE is a theorem, thus eliminating it as a hypothesis while assuming ax-ac2 as an axiom. (Contributed by Mario Carneiro, 6-May-2015) (Revised by NM, 20-Dec-2016) (Proof modification is discouraged.)

Ref Expression
Assertion axac3 ⊢ CHOICE

Proof

Step Hyp Ref Expression
1 ax-ac2 ⊢ ∃ y ∀ z ∃ w ∀ v y ∈ x ∧ z ∈ y → w ∈ x ∧ ¬ y = w ∧ z ∈ w ∨ ¬ y ∈ x ∧ z ∈ x → w ∈ z ∧ w ∈ y ∧ v ∈ z ∧ v ∈ y → v = w
2 1 ax-gen ⊢ ∀ x ∃ y ∀ z ∃ w ∀ v y ∈ x ∧ z ∈ y → w ∈ x ∧ ¬ y = w ∧ z ∈ w ∨ ¬ y ∈ x ∧ z ∈ x → w ∈ z ∧ w ∈ y ∧ v ∈ z ∧ v ∈ y → v = w
3 dfackm ⊢ CHOICE ↔ ∀ x ∃ y ∀ z ∃ w ∀ v y ∈ x ∧ z ∈ y → w ∈ x ∧ ¬ y = w ∧ z ∈ w ∨ ¬ y ∈ x ∧ z ∈ x → w ∈ z ∧ w ∈ y ∧ v ∈ z ∧ v ∈ y → v = w
4 2 3 mpbir ⊢ CHOICE