Theorem trcleq2lem

Description: Equality implies bijection. (Contributed by RP, 5-May-2020)

	Ref	Expression
Assertion	trcleq2lem	$$⊢A=B\to \left(\left(R\subseteq A\wedge A\circ A\subseteq A\right)\leftrightarrow \left(R\subseteq B\wedge B\circ B\subseteq B\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		sseq2	$$⊢A=B\to \left(R\subseteq A\leftrightarrow R\subseteq B\right)$$
2		id	$$⊢A=B\to A=B$$
3	2 2	coeq12d	$$⊢A=B\to A\circ A=B\circ B$$
4	3 2	sseq12d	$$⊢A=B\to \left(A\circ A\subseteq A\leftrightarrow B\circ B\subseteq B\right)$$
5	1 4	anbi12d	$$⊢A=B\to \left(\left(R\subseteq A\wedge A\circ A\subseteq A\right)\leftrightarrow \left(R\subseteq B\wedge B\circ B\subseteq B\right)\right)$$