Theorem cardeq0

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

	Ref	Expression
Assertion	cardeq0	|- ( A e. V -> ( ( card ` A ) = (/) <-> A = (/) ) )

Proof

Step	Hyp	Ref	Expression
1		0ex	|- (/) e. _V
2		carden	|- ( ( A e. V /\ (/) e. _V ) -> ( ( card ` A ) = ( card ` (/) ) <-> A ~~ (/) ) )
3	1 2	mpan2	|- ( A e. V -> ( ( card ` A ) = ( card ` (/) ) <-> A ~~ (/) ) )
4		card0	|- ( card ` (/) ) = (/)
5	4	eqeq2i	|- ( ( card ` A ) = ( card ` (/) ) <-> ( card ` A ) = (/) )
6		en0	|- ( A ~~ (/) <-> A = (/) )
7	3 5 6	3bitr3g	|- ( A e. V -> ( ( card ` A ) = (/) <-> A = (/) ) )