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 ( 𝑅 = 𝑆 → ( SymRel 𝑅 ↔ SymRel 𝑆 ) )

Proof

Step Hyp Ref Expression
1 cnveq ( 𝑅 = 𝑆 𝑅 = 𝑆 )
2 id ( 𝑅 = 𝑆𝑅 = 𝑆 )
3 1 2 sseq12d ( 𝑅 = 𝑆 → ( 𝑅𝑅 𝑆𝑆 ) )
4 releq ( 𝑅 = 𝑆 → ( Rel 𝑅 ↔ Rel 𝑆 ) )
5 3 4 anbi12d ( 𝑅 = 𝑆 → ( ( 𝑅𝑅 ∧ Rel 𝑅 ) ↔ ( 𝑆𝑆 ∧ Rel 𝑆 ) ) )
6 dfsymrel2 ( SymRel 𝑅 ↔ ( 𝑅𝑅 ∧ Rel 𝑅 ) )
7 dfsymrel2 ( SymRel 𝑆 ↔ ( 𝑆𝑆 ∧ Rel 𝑆 ) )
8 5 6 7 3bitr4g ( 𝑅 = 𝑆 → ( SymRel 𝑅 ↔ SymRel 𝑆 ) )