Theorem cardidg

Description: Any set is equinumerous to its cardinal number. Closed theorem form of cardid . (Contributed by David Moews, 1-May-2017)

	Ref	Expression
Assertion	cardidg	|- ( A e. B -> ( card ` A ) ~~ A )

Proof

Step	Hyp	Ref	Expression
1		elex	|- ( A e. B -> A e. _V )
2		cardeqv	|- dom card = _V
3	2	eleq2i	|- ( A e. dom card <-> A e. _V )
4		cardid2	|- ( A e. dom card -> ( card ` A ) ~~ A )
5	3 4	sylbir	|- ( A e. _V -> ( card ` A ) ~~ A )
6	1 5	syl	|- ( A e. B -> ( card ` A ) ~~ A )