Theorem relnonrel

Description: The non-relation part of a relation is empty. (Contributed by RP, 22-Oct-2020)

	Ref	Expression
Assertion	relnonrel	$$⊢\mathrm{Rel}A\leftrightarrow A\setminus {A^{-1}}^{-1}=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		dfrel2	$$⊢\mathrm{Rel}A\leftrightarrow {A^{-1}}^{-1}=A$$
2		eqss	$$⊢{A^{-1}}^{-1}=A\leftrightarrow \left({A^{-1}}^{-1}\subseteq A\wedge A\subseteq {A^{-1}}^{-1}\right)$$
3	1 2	bitri	$$⊢\mathrm{Rel}A\leftrightarrow \left({A^{-1}}^{-1}\subseteq A\wedge A\subseteq {A^{-1}}^{-1}\right)$$
4		cnvcnvss	$$⊢{A^{-1}}^{-1}\subseteq A$$
5	4	biantrur	$$⊢A\subseteq {A^{-1}}^{-1}\leftrightarrow \left({A^{-1}}^{-1}\subseteq A\wedge A\subseteq {A^{-1}}^{-1}\right)$$
6		ssdif0	$$⊢A\subseteq {A^{-1}}^{-1}\leftrightarrow A\setminus {A^{-1}}^{-1}=\varnothing$$
7	3 5 6	3bitr2i	$$⊢\mathrm{Rel}A\leftrightarrow A\setminus {A^{-1}}^{-1}=\varnothing$$