Metamath Proof Explorer

Theorem cnveqi

Description: Equality inference for converse relation. (Contributed by NM, 23-Dec-2008)

Ref Expression
Hypothesis cnveqi.1 
|- A = B
Assertion cnveqi 
|- `' A = `' B

Proof

Step Hyp Ref Expression
1 cnveqi.1 
 |-  A = B
2 cnveq 
 |-  ( A = B -> `' A = `' B )
3 1 2 ax-mp 
 |-  `' A = `' B