Theorem cnveq0

Description: A relation is empty iff its converse is empty. (Contributed by FL, 19-Sep-2011)

	Ref	Expression
Assertion	cnveq0	$$⊢\mathrm{Rel}A\to \left(A=\varnothing \leftrightarrow A^{-1}=\varnothing \right)$$

Proof

Step	Hyp	Ref	Expression
1		rel0	$$⊢\mathrm{Rel}\varnothing$$
2		cnveqb	$$⊢\left(\mathrm{Rel}A\wedge \mathrm{Rel}\varnothing \right)\to \left(A=\varnothing \leftrightarrow A^{-1}={\varnothing }^{-1}\right)$$
3	1 2	mpan2	$$⊢\mathrm{Rel}A\to \left(A=\varnothing \leftrightarrow A^{-1}={\varnothing }^{-1}\right)$$
4		cnv0	$$⊢{\varnothing }^{-1}=\varnothing$$
5	4	eqeq2i	$$⊢A^{-1}={\varnothing }^{-1}\leftrightarrow A^{-1}=\varnothing$$
6	3 5	bitrdi	$$⊢\mathrm{Rel}A\to \left(A=\varnothing \leftrightarrow A^{-1}=\varnothing \right)$$