Theorem trreleq

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

	Ref	Expression
Assertion	trreleq	⊢ ( 𝑅 = 𝑆 → ( TrRel 𝑅 ↔ TrRel 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		coideq	⊢ ( 𝑅 = 𝑆 → ( 𝑅 ∘ 𝑅 ) = ( 𝑆 ∘ 𝑆 ) )
2		id	⊢ ( 𝑅 = 𝑆 → 𝑅 = 𝑆 )
3	1 2	sseq12d	⊢ ( 𝑅 = 𝑆 → ( ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ↔ ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ) )
4		releq	⊢ ( 𝑅 = 𝑆 → ( Rel 𝑅 ↔ Rel 𝑆 ) )
5	3 4	anbi12d	⊢ ( 𝑅 = 𝑆 → ( ( ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ∧ Rel 𝑅 ) ↔ ( ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ∧ Rel 𝑆 ) ) )
6		dftrrel2	⊢ ( TrRel 𝑅 ↔ ( ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ∧ Rel 𝑅 ) )
7		dftrrel2	⊢ ( TrRel 𝑆 ↔ ( ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ∧ Rel 𝑆 ) )
8	5 6 7	3bitr4g	⊢ ( 𝑅 = 𝑆 → ( TrRel 𝑅 ↔ TrRel 𝑆 ) )