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		cnveq	$$⊢A=B\to A^{-1}=B^{-1}$$
2		dfrel2	$$⊢\mathrm{Rel}A\leftrightarrow {A^{-1}}^{-1}=A$$
3		dfrel2	$$⊢\mathrm{Rel}B\leftrightarrow {B^{-1}}^{-1}=B$$
4		cnveq	$$⊢A^{-1}=B^{-1}\to {A^{-1}}^{-1}={B^{-1}}^{-1}$$
5		eqeq2	$$⊢B={B^{-1}}^{-1}\to \left({A^{-1}}^{-1}=B\leftrightarrow {A^{-1}}^{-1}={B^{-1}}^{-1}\right)$$
6	4 5	imbitrrid	$$⊢B={B^{-1}}^{-1}\to \left(A^{-1}=B^{-1}\to {A^{-1}}^{-1}=B\right)$$
7	6	eqcoms	$$⊢{B^{-1}}^{-1}=B\to \left(A^{-1}=B^{-1}\to {A^{-1}}^{-1}=B\right)$$
8	3 7	sylbi	$$⊢\mathrm{Rel}B\to \left(A^{-1}=B^{-1}\to {A^{-1}}^{-1}=B\right)$$
9		eqeq1	$$⊢A={A^{-1}}^{-1}\to \left(A=B\leftrightarrow {A^{-1}}^{-1}=B\right)$$
10	9	imbi2d	$$⊢A={A^{-1}}^{-1}\to \left(\left(A^{-1}=B^{-1}\to A=B\right)\leftrightarrow \left(A^{-1}=B^{-1}\to {A^{-1}}^{-1}=B\right)\right)$$
11	8 10	imbitrrid	$$⊢A={A^{-1}}^{-1}\to \left(\mathrm{Rel}B\to \left(A^{-1}=B^{-1}\to A=B\right)\right)$$
12	11	eqcoms	$$⊢{A^{-1}}^{-1}=A\to \left(\mathrm{Rel}B\to \left(A^{-1}=B^{-1}\to A=B\right)\right)$$
13	2 12	sylbi	$$⊢\mathrm{Rel}A\to \left(\mathrm{Rel}B\to \left(A^{-1}=B^{-1}\to A=B\right)\right)$$
14	13	imp	$$⊢\left(\mathrm{Rel}A\wedge \mathrm{Rel}B\right)\to \left(A^{-1}=B^{-1}\to A=B\right)$$
15	1 14	impbid2	$$⊢\left(\mathrm{Rel}A\wedge \mathrm{Rel}B\right)\to \left(A=B\leftrightarrow A^{-1}=B^{-1}\right)$$