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 |
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 |