Theorem cnveq0

Description: A relation 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		cnv0	$$⊢{\varnothing }^{-1}=\varnothing$$
2		rel0	$$⊢\mathrm{Rel}\varnothing$$
3		cnveqb	$$⊢\left(\mathrm{Rel}A\wedge \mathrm{Rel}\varnothing \right)\to \left(A=\varnothing \leftrightarrow A^{-1}={\varnothing }^{-1}\right)$$
4	2 3	mpan2	$$⊢\mathrm{Rel}A\to \left(A=\varnothing \leftrightarrow A^{-1}={\varnothing }^{-1}\right)$$
5		eqeq2	$$⊢\varnothing ={\varnothing }^{-1}\to \left(A^{-1}=\varnothing \leftrightarrow A^{-1}={\varnothing }^{-1}\right)$$
6	5	bibi2d	$$⊢\varnothing ={\varnothing }^{-1}\to \left(\left(A=\varnothing \leftrightarrow A^{-1}=\varnothing \right)\leftrightarrow \left(A=\varnothing \leftrightarrow A^{-1}={\varnothing }^{-1}\right)\right)$$
7	4 6	syl5ibr	$$⊢\varnothing ={\varnothing }^{-1}\to \left(\mathrm{Rel}A\to \left(A=\varnothing \leftrightarrow A^{-1}=\varnothing \right)\right)$$
8	7	eqcoms	$$⊢{\varnothing }^{-1}=\varnothing \to \left(\mathrm{Rel}A\to \left(A=\varnothing \leftrightarrow A^{-1}=\varnothing \right)\right)$$
9	1 8	ax-mp	$$⊢\mathrm{Rel}A\to \left(A=\varnothing \leftrightarrow A^{-1}=\varnothing \right)$$