Theorem cardnueq0

Description: The empty set is the only numerable set with cardinality zero. (Contributed by Mario Carneiro, 7-Jan-2013)

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

Proof

Step	Hyp	Ref	Expression
1		cardid2	$$⊢A\in \mathrm{dom}\mathrm{card}\to \mathrm{card}\left(A\right)\approx A$$
2	1	ensymd	$$⊢A\in \mathrm{dom}\mathrm{card}\to A\approx \mathrm{card}\left(A\right)$$
3		breq2	$$⊢\mathrm{card}\left(A\right)=\varnothing \to \left(A\approx \mathrm{card}\left(A\right)\leftrightarrow A\approx \varnothing \right)$$
4		en0	$$⊢A\approx \varnothing \leftrightarrow A=\varnothing$$
5	3 4	bitrdi	$$⊢\mathrm{card}\left(A\right)=\varnothing \to \left(A\approx \mathrm{card}\left(A\right)\leftrightarrow A=\varnothing \right)$$
6	2 5	syl5ibcom	$$⊢A\in \mathrm{dom}\mathrm{card}\to \left(\mathrm{card}\left(A\right)=\varnothing \to A=\varnothing \right)$$
7		fveq2	$$⊢A=\varnothing \to \mathrm{card}\left(A\right)=\mathrm{card}\left(\varnothing \right)$$
8		card0	$$⊢\mathrm{card}\left(\varnothing \right)=\varnothing$$
9	7 8	eqtrdi	$$⊢A=\varnothing \to \mathrm{card}\left(A\right)=\varnothing$$
10	6 9	impbid1	$$⊢A\in \mathrm{dom}\mathrm{card}\to \left(\mathrm{card}\left(A\right)=\varnothing \leftrightarrow A=\varnothing \right)$$