Metamath Proof Explorer

Theorem dfac10c

Description: Axiom of Choice equivalent: every set is equinumerous to an ordinal. (Contributed by Stefan O'Rear, 17-Jan-2015)

Ref Expression
Assertion dfac10c 
|- ( CHOICE <-> A. x E. y e. On y ~~ x )

Proof

Step Hyp Ref Expression
1 dfac10 
 |-  ( CHOICE <-> dom card = _V )
2 eqv 
 |-  ( dom card = _V <-> A. x x e. dom card )
3 isnum2 
 |-  ( x e. dom card <-> E. y e. On y ~~ x )
4 3 albii 
 |-  ( A. x x e. dom card <-> A. x E. y e. On y ~~ x )
5 1 2 4 3bitri 
 |-  ( CHOICE <-> A. x E. y e. On y ~~ x )