Theorem cardeq0

Description: Only the empty set has cardinality zero. (Contributed by NM, 23-Apr-2004)

	Ref	Expression
Assertion	cardeq0	⊢ ( 𝐴 ∈ 𝑉 → ( ( card ‘ 𝐴 ) = ∅ ↔ 𝐴 = ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		0ex	⊢ ∅ ∈ V
2		carden	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∅ ∈ V ) → ( ( card ‘ 𝐴 ) = ( card ‘ ∅ ) ↔ 𝐴 ≈ ∅ ) )
3	1 2	mpan2	⊢ ( 𝐴 ∈ 𝑉 → ( ( card ‘ 𝐴 ) = ( card ‘ ∅ ) ↔ 𝐴 ≈ ∅ ) )
4		card0	⊢ ( card ‘ ∅ ) = ∅
5	4	eqeq2i	⊢ ( ( card ‘ 𝐴 ) = ( card ‘ ∅ ) ↔ ( card ‘ 𝐴 ) = ∅ )
6		en0	⊢ ( 𝐴 ≈ ∅ ↔ 𝐴 = ∅ )
7	3 5 6	3bitr3g	⊢ ( 𝐴 ∈ 𝑉 → ( ( card ‘ 𝐴 ) = ∅ ↔ 𝐴 = ∅ ) )