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 )