Metamath Proof Explorer


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 syl5ibr
 |-  ( 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 syl5ibr
 |-  ( 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 ) )