Theorem kard0b

Description: The empty set is the only set with cardinality zero. This is the kard version of cardeq0 . (Contributed by BTernaryTau, 3-Jul-2026)

	Ref	Expression
Assertion	kard0b	|- ( ( kard ` A ) = ( kard ` (/) ) <-> A = (/) )

Proof

Step	Hyp	Ref	Expression
1		kardeng	|- ( A e. _V -> ( ( kard ` A ) = ( kard ` (/) ) <-> A ~~ (/) ) )
2		en0	|- ( A ~~ (/) <-> A = (/) )
3	1 2	bitrdi	|- ( A e. _V -> ( ( kard ` A ) = ( kard ` (/) ) <-> A = (/) ) )
4		fvprc	|- ( -. A e. _V -> ( kard ` A ) = (/) )
5		0nep0	|- (/) =/= { (/) }
6		kard0	|- ( kard ` (/) ) = { (/) }
7	5 6	neeqtrri	|- (/) =/= ( kard ` (/) )
8	7	a1i	|- ( -. A e. _V -> (/) =/= ( kard ` (/) ) )
9	4 8	eqnetrd	|- ( -. A e. _V -> ( kard ` A ) =/= ( kard ` (/) ) )
10	9	neneqd	|- ( -. A e. _V -> -. ( kard ` A ) = ( kard ` (/) ) )
11		0ex	|- (/) e. _V
12		eleq1	|- ( A = (/) -> ( A e. _V <-> (/) e. _V ) )
13	11 12	mpbiri	|- ( A = (/) -> A e. _V )
14	13	con3i	|- ( -. A e. _V -> -. A = (/) )
15	10 14	2falsed	|- ( -. A e. _V -> ( ( kard ` A ) = ( kard ` (/) ) <-> A = (/) ) )
16	3 15	pm2.61i	|- ( ( kard ` A ) = ( kard ` (/) ) <-> A = (/) )