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	$$⊢A=\varnothing \leftrightarrow \left(\mathrm{Rel}A\wedge A^{-1}=\varnothing \right)$$

Proof

Step	Hyp	Ref	Expression
1		rel0	$$⊢\mathrm{Rel}\varnothing$$
2		releq	$$⊢A=\varnothing \to \left(\mathrm{Rel}A\leftrightarrow \mathrm{Rel}\varnothing \right)$$
3	1 2	mpbiri	$$⊢A=\varnothing \to \mathrm{Rel}A$$
4		cnveq0	$$⊢\mathrm{Rel}A\to \left(A=\varnothing \leftrightarrow A^{-1}=\varnothing \right)$$
5	3 4	biadanii	$$⊢A=\varnothing \leftrightarrow \left(\mathrm{Rel}A\wedge A^{-1}=\varnothing \right)$$