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 ‘ 𝐴 ) = ( kard ‘ ∅ ) ↔ 𝐴 = ∅ )

Proof

Step	Hyp	Ref	Expression
1		kardeng	⊢ ( 𝐴 ∈ V → ( ( kard ‘ 𝐴 ) = ( kard ‘ ∅ ) ↔ 𝐴 ≈ ∅ ) )
2		en0	⊢ ( 𝐴 ≈ ∅ ↔ 𝐴 = ∅ )
3	1 2	bitrdi	⊢ ( 𝐴 ∈ V → ( ( kard ‘ 𝐴 ) = ( kard ‘ ∅ ) ↔ 𝐴 = ∅ ) )
4		fvprc	⊢ ( ¬ 𝐴 ∈ V → ( kard ‘ 𝐴 ) = ∅ )
5		0nep0	⊢ ∅ ≠ { ∅ }
6		kard0	⊢ ( kard ‘ ∅ ) = { ∅ }
7	5 6	neeqtrri	⊢ ∅ ≠ ( kard ‘ ∅ )
8	7	a1i	⊢ ( ¬ 𝐴 ∈ V → ∅ ≠ ( kard ‘ ∅ ) )
9	4 8	eqnetrd	⊢ ( ¬ 𝐴 ∈ V → ( kard ‘ 𝐴 ) ≠ ( kard ‘ ∅ ) )
10	9	neneqd	⊢ ( ¬ 𝐴 ∈ V → ¬ ( kard ‘ 𝐴 ) = ( kard ‘ ∅ ) )
11		0ex	⊢ ∅ ∈ V
12		eleq1	⊢ ( 𝐴 = ∅ → ( 𝐴 ∈ V ↔ ∅ ∈ V ) )
13	11 12	mpbiri	⊢ ( 𝐴 = ∅ → 𝐴 ∈ V )
14	13	con3i	⊢ ( ¬ 𝐴 ∈ V → ¬ 𝐴 = ∅ )
15	10 14	2falsed	⊢ ( ¬ 𝐴 ∈ V → ( ( kard ‘ 𝐴 ) = ( kard ‘ ∅ ) ↔ 𝐴 = ∅ ) )
16	3 15	pm2.61i	⊢ ( ( kard ‘ 𝐴 ) = ( kard ‘ ∅ ) ↔ 𝐴 = ∅ )