Metamath Proof Explorer


Theorem cardval2

Description: An alternate version of the value of the cardinal number of a set. Compare cardval . This theorem could be used to give a simpler definition of card in place of df-card . It apparently does not occur in the literature. (Contributed by NM, 7-Nov-2003)

Ref Expression
Assertion cardval2 A dom card card A = x On | x A

Proof

Step Hyp Ref Expression
1 cardsdomel x On A dom card x A x card A
2 1 ancoms A dom card x On x A x card A
3 2 pm5.32da A dom card x On x A x On x card A
4 cardon card A On
5 4 oneli x card A x On
6 5 pm4.71ri x card A x On x card A
7 3 6 syl6rbbr A dom card x card A x On x A
8 7 abbi2dv A dom card card A = x | x On x A
9 df-rab x On | x A = x | x On x A
10 8 9 eqtr4di A dom card card A = x On | x A