Theorem cnveq0b

Description: A class is empty iff it is a relation whose converse is empty. (Contributed by SN, 8-Oct-2026)

	Ref	Expression
Assertion	cnveq0b	⊢ ( 𝐴 = ∅ ↔ ( Rel 𝐴 ∧ ◡ 𝐴 = ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		rel0	⊢ Rel ∅
2		releq	⊢ ( 𝐴 = ∅ → ( Rel 𝐴 ↔ Rel ∅ ) )
3	1 2	mpbiri	⊢ ( 𝐴 = ∅ → Rel 𝐴 )
4		cnveq0	⊢ ( Rel 𝐴 → ( 𝐴 = ∅ ↔ ◡ 𝐴 = ∅ ) )
5	3 4	biadanii	⊢ ( 𝐴 = ∅ ↔ ( Rel 𝐴 ∧ ◡ 𝐴 = ∅ ) )