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 𝑆 ) )