Theorem cardennn

Description: If A is equinumerous to a natural number, then that number is its cardinal. (Contributed by Mario Carneiro, 11-Jan-2013)

	Ref	Expression
Assertion	cardennn	$$⊢\left(A\approx B\wedge B\in \mathrm{\omega }\right)\to \mathrm{card}\left(A\right)=B$$

Proof

Step	Hyp	Ref	Expression
1		carden2b	$$⊢A\approx B\to \mathrm{card}\left(A\right)=\mathrm{card}\left(B\right)$$
2		cardnn	$$⊢B\in \mathrm{\omega }\to \mathrm{card}\left(B\right)=B$$
3	1 2	sylan9eq	$$⊢\left(A\approx B\wedge B\in \mathrm{\omega }\right)\to \mathrm{card}\left(A\right)=B$$