Theorem cnveqb

Description: Equality theorem for converse. (Contributed by FL, 19-Sep-2011)

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

Proof

Step	Hyp	Ref	Expression
1		cnvssb	$$⊢\mathrm{Rel}A\to \left(A\subseteq B\leftrightarrow A^{-1}\subseteq B^{-1}\right)$$
2		cnvssb	$$⊢\mathrm{Rel}B\to \left(B\subseteq A\leftrightarrow B^{-1}\subseteq A^{-1}\right)$$
3	1 2	bi2anan9	$$⊢\left(\mathrm{Rel}A\wedge \mathrm{Rel}B\right)\to \left(\left(A\subseteq B\wedge B\subseteq A\right)\leftrightarrow \left(A^{-1}\subseteq B^{-1}\wedge B^{-1}\subseteq A^{-1}\right)\right)$$
4		eqss	$$⊢A=B\leftrightarrow \left(A\subseteq B\wedge B\subseteq A\right)$$
5		eqss	$$⊢A^{-1}=B^{-1}\leftrightarrow \left(A^{-1}\subseteq B^{-1}\wedge B^{-1}\subseteq A^{-1}\right)$$
6	3 4 5	3bitr4g	$$⊢\left(\mathrm{Rel}A\wedge \mathrm{Rel}B\right)\to \left(A=B\leftrightarrow A^{-1}=B^{-1}\right)$$