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	|- ( R = S -> ( TrRel R <-> TrRel S ) )

Proof

Step	Hyp	Ref	Expression
1		coideq	|- ( R = S -> ( R o. R ) = ( S o. S ) )
2		id	|- ( R = S -> R = S )
3	1 2	sseq12d	|- ( R = S -> ( ( R o. R ) C_ R <-> ( S o. S ) C_ S ) )
4		releq	|- ( R = S -> ( Rel R <-> Rel S ) )
5	3 4	anbi12d	|- ( R = S -> ( ( ( R o. R ) C_ R /\ Rel R ) <-> ( ( S o. S ) C_ S /\ Rel S ) ) )
6		dftrrel2	|- ( TrRel R <-> ( ( R o. R ) C_ R /\ Rel R ) )
7		dftrrel2	|- ( TrRel S <-> ( ( S o. S ) C_ S /\ Rel S ) )
8	5 6 7	3bitr4g	|- ( R = S -> ( TrRel R <-> TrRel S ) )