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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vex | |
|
2 | 1 | elima | |
3 | 2 | bicomi | |
4 | 3 | albii | |
5 | dfac10c | |
|
6 | eqv | |
|
7 | 4 5 6 | 3bitr4i | |