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

Metamath Proof Explorer

Theorem releqi

Description: Equality inference for the relation predicate. (Contributed by NM, 8-Dec-2006)

Ref Expression
Hypothesis releqi.1 
|- A = B
Assertion releqi 
|- ( Rel A <-> Rel B )

Proof

Step Hyp Ref Expression
1 releqi.1 
 |-  A = B
2 releq 
 |-  ( A = B -> ( Rel A <-> Rel B ) )
3 1 2 ax-mp 
 |-  ( Rel A <-> Rel B )