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 |