Metamath Proof Explorer

Theorem symreleq

Description: Equality theorem for symmetric relation. (Contributed by Peter Mazsa, 15-Apr-2019) (Revised by Peter Mazsa, 23-Sep-2021)

Ref Expression
Assertion symreleq 
|- ( R = S -> ( SymRel R <-> SymRel S ) )

Proof

Step Hyp Ref Expression
1 cnveq 
 |-  ( R = S -> `' R = `' S )
2 id 
 |-  ( R = S -> R = S )
3 1 2 sseq12d 
 |-  ( R = S -> ( `' R C_ R <-> `' S C_ S ) )
4 releq 
 |-  ( R = S -> ( Rel R <-> Rel S ) )
5 3 4 anbi12d 
 |-  ( R = S -> ( ( `' R C_ R /\ Rel R ) <-> ( `' S C_ S /\ Rel S ) ) )
6 dfsymrel2 
 |-  ( SymRel R <-> ( `' R C_ R /\ Rel R ) )
7 dfsymrel2 
 |-  ( SymRel S <-> ( `' S C_ S /\ Rel S ) )
8 5 6 7 3bitr4g 
 |-  ( R = S -> ( SymRel R <-> SymRel S ) )