This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 \to (TrRel R \leftrightarrow TrRel S)$

Proof

Step	Hyp	Ref	Expression
1		coideq	$⊢ R = S \to R \circ R = S \circ S$
2		id	$⊢ R = S \to R = S$
3	1 2	sseq12d	$⊢ R = S \to (R \circ R \subseteq R \leftrightarrow S \circ S \subseteq S)$
4		releq	$⊢ R = S \to (Rel R \leftrightarrow Rel S)$
5	3 4	anbi12d	$⊢ R = S \to ((R \circ R \subseteq R \land Rel R) \leftrightarrow (S \circ S \subseteq S \land Rel S))$
6		dftrrel2	$⊢ TrRel R \leftrightarrow (R \circ R \subseteq R \land Rel R)$
7		dftrrel2	$⊢ TrRel S \leftrightarrow (S \circ S \subseteq S \land Rel S)$
8	5 6 7	3bitr4g	$⊢ R = S \to (TrRel R \leftrightarrow TrRel S)$