Description: Axiom of Choice equivalent: every set is equinumerous to an ordinal (quantifier-free short cryptic version alluded to in df-ac ). (Contributed by Stefan O'Rear, 17-Jan-2015)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | dfac10b | |- ( CHOICE <-> ( ~~ " On ) = _V ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | vex | |- x e. _V |
|
| 2 | 1 | elima | |- ( x e. ( ~~ " On ) <-> E. y e. On y ~~ x ) |
| 3 | 2 | bicomi | |- ( E. y e. On y ~~ x <-> x e. ( ~~ " On ) ) |
| 4 | 3 | albii | |- ( A. x E. y e. On y ~~ x <-> A. x x e. ( ~~ " On ) ) |
| 5 | dfac10c | |- ( CHOICE <-> A. x E. y e. On y ~~ x ) |
|
| 6 | eqv | |- ( ( ~~ " On ) = _V <-> A. x x e. ( ~~ " On ) ) |
|
| 7 | 4 5 6 | 3bitr4i | |- ( CHOICE <-> ( ~~ " On ) = _V ) |