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
 |-  E. y A. z E. w A. v ( ( y e. x /\ ( z e. y -> ( ( w e. x /\ -. y = w ) /\ z e. w ) ) ) \/ ( -. y e. x /\ ( z e. x -> ( ( w e. z /\ w e. y ) /\ ( ( v e. z /\ v e. y ) -> v = w ) ) ) ) )
2 1 ax-gen
 |-  A. x E. y A. z E. w A. v ( ( y e. x /\ ( z e. y -> ( ( w e. x /\ -. y = w ) /\ z e. w ) ) ) \/ ( -. y e. x /\ ( z e. x -> ( ( w e. z /\ w e. y ) /\ ( ( v e. z /\ v e. y ) -> v = w ) ) ) ) )
3 dfackm
 |-  ( CHOICE <-> A. x E. y A. z E. w A. v ( ( y e. x /\ ( z e. y -> ( ( w e. x /\ -. y = w ) /\ z e. w ) ) ) \/ ( -. y e. x /\ ( z e. x -> ( ( w e. z /\ w e. y ) /\ ( ( v e. z /\ v e. y ) -> v = w ) ) ) ) ) )
4 2 3 mpbir
 |-  CHOICE