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 𝑦𝑧𝑤𝑣 ( ( 𝑦𝑥 ∧ ( 𝑧𝑦 → ( ( 𝑤𝑥 ∧ ¬ 𝑦 = 𝑤 ) ∧ 𝑧𝑤 ) ) ) ∨ ( ¬ 𝑦𝑥 ∧ ( 𝑧𝑥 → ( ( 𝑤𝑧𝑤𝑦 ) ∧ ( ( 𝑣𝑧𝑣𝑦 ) → 𝑣 = 𝑤 ) ) ) ) )
2 1 ax-gen 𝑥𝑦𝑧𝑤𝑣 ( ( 𝑦𝑥 ∧ ( 𝑧𝑦 → ( ( 𝑤𝑥 ∧ ¬ 𝑦 = 𝑤 ) ∧ 𝑧𝑤 ) ) ) ∨ ( ¬ 𝑦𝑥 ∧ ( 𝑧𝑥 → ( ( 𝑤𝑧𝑤𝑦 ) ∧ ( ( 𝑣𝑧𝑣𝑦 ) → 𝑣 = 𝑤 ) ) ) ) )
3 dfackm ( CHOICE ↔ ∀ 𝑥𝑦𝑧𝑤𝑣 ( ( 𝑦𝑥 ∧ ( 𝑧𝑦 → ( ( 𝑤𝑥 ∧ ¬ 𝑦 = 𝑤 ) ∧ 𝑧𝑤 ) ) ) ∨ ( ¬ 𝑦𝑥 ∧ ( 𝑧𝑥 → ( ( 𝑤𝑧𝑤𝑦 ) ∧ ( ( 𝑣𝑧𝑣𝑦 ) → 𝑣 = 𝑤 ) ) ) ) ) )
4 2 3 mpbir CHOICE