This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZFC (ZERMELO-FRAENKEL WITH CHOICE) SET THEORY ZFC Set Theory - add the Axiom of Choice Introduce the Axiom of Choice 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