Theorem card0

Description: The cardinality of the empty set is the empty set. (Contributed by NM, 25-Oct-2003)

	Ref	Expression
Assertion	card0	$$⊢\mathrm{card}\left(\varnothing \right)=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		0elon	$$⊢\varnothing \in \mathrm{On}$$
2		cardonle	$$⊢\varnothing \in \mathrm{On}\to \mathrm{card}\left(\varnothing \right)\subseteq \varnothing$$
3	1 2	ax-mp	$$⊢\mathrm{card}\left(\varnothing \right)\subseteq \varnothing$$
4		ss0b	$$⊢\mathrm{card}\left(\varnothing \right)\subseteq \varnothing \leftrightarrow \mathrm{card}\left(\varnothing \right)=\varnothing$$
5	3 4	mpbi	$$⊢\mathrm{card}\left(\varnothing \right)=\varnothing$$