Metamath Proof Explorer


Theorem dfac10b

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 CHOICEOn=V

Proof

Step Hyp Ref Expression
1 vex xV
2 1 elima xOnyOnyx
3 2 bicomi yOnyxxOn
4 3 albii xyOnyxxxOn
5 dfac10c CHOICExyOnyx
6 eqv On=VxxOn
7 4 5 6 3bitr4i CHOICEOn=V