Theorem cardeq0

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

	Ref	Expression
Assertion	cardeq0	$$⊢A\in V\to \left(\mathrm{card}\left(A\right)=\varnothing \leftrightarrow A=\varnothing \right)$$

Proof

Step	Hyp	Ref	Expression
1		0ex	$$⊢\varnothing \in \mathrm{V}$$
2		carden	$$⊢\left(A\in V\wedge \varnothing \in \mathrm{V}\right)\to \left(\mathrm{card}\left(A\right)=\mathrm{card}\left(\varnothing \right)\leftrightarrow A\approx \varnothing \right)$$
3	1 2	mpan2	$$⊢A\in V\to \left(\mathrm{card}\left(A\right)=\mathrm{card}\left(\varnothing \right)\leftrightarrow A\approx \varnothing \right)$$
4		card0	$$⊢\mathrm{card}\left(\varnothing \right)=\varnothing$$
5	4	eqeq2i	$$⊢\mathrm{card}\left(A\right)=\mathrm{card}\left(\varnothing \right)\leftrightarrow \mathrm{card}\left(A\right)=\varnothing$$
6		en0	$$⊢A\approx \varnothing \leftrightarrow A=\varnothing$$
7	3 5 6	3bitr3g	$$⊢A\in V\to \left(\mathrm{card}\left(A\right)=\varnothing \leftrightarrow A=\varnothing \right)$$