Theorem cnveqb

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

	Ref	Expression
Assertion	cnveqb	|- ( ( Rel A /\ Rel B ) -> ( A = B <-> `' A = `' B ) )

Proof

Step	Hyp	Ref	Expression
1		cnveq	|- ( A = B -> `' A = `' B )
2		dfrel2	|- ( Rel A <-> `' `' A = A )
3		dfrel2	|- ( Rel B <-> `' `' B = B )
4		cnveq	|- ( `' A = `' B -> `' `' A = `' `' B )
5		eqeq2	|- ( B = `' `' B -> ( `' `' A = B <-> `' `' A = `' `' B ) )
6	4 5	imbitrrid	|- ( B = `' `' B -> ( `' A = `' B -> `' `' A = B ) )
7	6	eqcoms	|- ( `' `' B = B -> ( `' A = `' B -> `' `' A = B ) )
8	3 7	sylbi	|- ( Rel B -> ( `' A = `' B -> `' `' A = B ) )
9		eqeq1	|- ( A = `' `' A -> ( A = B <-> `' `' A = B ) )
10	9	imbi2d	|- ( A = `' `' A -> ( ( `' A = `' B -> A = B ) <-> ( `' A = `' B -> `' `' A = B ) ) )
11	8 10	imbitrrid	|- ( A = `' `' A -> ( Rel B -> ( `' A = `' B -> A = B ) ) )
12	11	eqcoms	|- ( `' `' A = A -> ( Rel B -> ( `' A = `' B -> A = B ) ) )
13	2 12	sylbi	|- ( Rel A -> ( Rel B -> ( `' A = `' B -> A = B ) ) )
14	13	imp	|- ( ( Rel A /\ Rel B ) -> ( `' A = `' B -> A = B ) )
15	1 14	impbid2	|- ( ( Rel A /\ Rel B ) -> ( A = B <-> `' A = `' B ) )