Metamath Proof Explorer

Theorem releqd

Description: Equality deduction for the relation predicate. (Contributed by NM, 8-Mar-2014)

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

Proof

Step Hyp Ref Expression
1 releqd.1 
 |-  ( ph -> A = B )
2 releq 
 |-  ( A = B -> ( Rel A <-> Rel B ) )
3 1 2 syl 
 |-  ( ph -> ( Rel A <-> Rel B ) )