Metamath Proof Explorer

Theorem releq

Description: Equality theorem for the relation predicate. (Contributed by NM, 1-Aug-1994)

Ref Expression
Assertion releq 
|- ( A = B -> ( Rel A <-> Rel B ) )

Proof

Step Hyp Ref Expression
1 sseq1 
 |-  ( A = B -> ( A C_ ( _V X. _V ) <-> B C_ ( _V X. _V ) ) )
2 df-rel 
 |-  ( Rel A <-> A C_ ( _V X. _V ) )
3 df-rel 
 |-  ( Rel B <-> B C_ ( _V X. _V ) )
4 1 2 3 3bitr4g 
 |-  ( A = B -> ( Rel A <-> Rel B ) )