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	Could not format assertion : No typesetting found for |- ( ( kard ` A ) = ( kard ` (/) ) <-> A = (/) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		kardeng	Could not format ( A e. _V -> ( ( kard ` A ) = ( kard ` (/) ) <-> A ~~ (/) ) ) : No typesetting found for |- ( A e. _V -> ( ( kard ` A ) = ( kard ` (/) ) <-> A ~~ (/) ) ) with typecode |-
2		en0	$$⊢A\approx \varnothing \leftrightarrow A=\varnothing$$
3	1 2	bitrdi	Could not format ( A e. _V -> ( ( kard ` A ) = ( kard ` (/) ) <-> A = (/) ) ) : No typesetting found for |- ( A e. _V -> ( ( kard ` A ) = ( kard ` (/) ) <-> A = (/) ) ) with typecode |-
4		fvprc	Could not format ( -. A e. _V -> ( kard ` A ) = (/) ) : No typesetting found for |- ( -. A e. _V -> ( kard ` A ) = (/) ) with typecode |-
5		0nep0	$$⊢\varnothing \ne \left\{\varnothing \right\}$$
6		kard0	Could not format ( kard ` (/) ) = { (/) } : No typesetting found for |- ( kard ` (/) ) = { (/) } with typecode |-
7	5 6	neeqtrri	Could not format (/) =/= ( kard ` (/) ) : No typesetting found for |- (/) =/= ( kard ` (/) ) with typecode |-
8	7	a1i	Could not format ( -. A e. _V -> (/) =/= ( kard ` (/) ) ) : No typesetting found for |- ( -. A e. _V -> (/) =/= ( kard ` (/) ) ) with typecode |-
9	4 8	eqnetrd	Could not format ( -. A e. _V -> ( kard ` A ) =/= ( kard ` (/) ) ) : No typesetting found for |- ( -. A e. _V -> ( kard ` A ) =/= ( kard ` (/) ) ) with typecode |-
10	9	neneqd	Could not format ( -. A e. _V -> -. ( kard ` A ) = ( kard ` (/) ) ) : No typesetting found for |- ( -. A e. _V -> -. ( kard ` A ) = ( kard ` (/) ) ) with typecode |-
11		0ex	$$⊢\varnothing \in \mathrm{V}$$
12		eleq1	$$⊢A=\varnothing \to \left(A\in \mathrm{V}\leftrightarrow \varnothing \in \mathrm{V}\right)$$
13	11 12	mpbiri	$$⊢A=\varnothing \to A\in \mathrm{V}$$
14	13	con3i	$$⊢\neg A\in \mathrm{V}\to \neg A=\varnothing$$
15	10 14	2falsed	Could not format ( -. A e. _V -> ( ( kard ` A ) = ( kard ` (/) ) <-> A = (/) ) ) : No typesetting found for |- ( -. A e. _V -> ( ( kard ` A ) = ( kard ` (/) ) <-> A = (/) ) ) with typecode |-
16	3 15	pm2.61i	Could not format ( ( kard ` A ) = ( kard ` (/) ) <-> A = (/) ) : No typesetting found for |- ( ( kard ` A ) = ( kard ` (/) ) <-> A = (/) ) with typecode |-