Theorem card0

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

	Ref	Expression
Assertion	card0	⊢ ( card ‘ ∅ ) = ∅

Proof

Step	Hyp	Ref	Expression
1		0elon	⊢ ∅ ∈ On
2		cardonle	⊢ ( ∅ ∈ On → ( card ‘ ∅ ) ⊆ ∅ )
3	1 2	ax-mp	⊢ ( card ‘ ∅ ) ⊆ ∅
4		ss0b	⊢ ( ( card ‘ ∅ ) ⊆ ∅ ↔ ( card ‘ ∅ ) = ∅ )
5	3 4	mpbi	⊢ ( card ‘ ∅ ) = ∅