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