This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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