Metamath Proof Explorer

Theorem numth3

Description: All sets are well-orderable under choice. (Contributed by Stefan O'Rear, 28-Feb-2015)

Ref Expression
Assertion numth3 
|- ( A e. V -> A e. dom card )

Proof

Step Hyp Ref Expression
1 elex 
 |-  ( A e. V -> A e. _V )
2 cardeqv 
 |-  dom card = _V
3 1 2 eleqtrrdi 
 |-  ( A e. V -> A e. dom card )