Theorem trcleq2lemRP

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

	Ref	Expression
Assertion	trcleq2lemRP	$$⊢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		id	$$⊢A=B\to A=B$$
2	1 1	coeq12d	$$⊢A=B\to A\circ A=B\circ B$$
3	2 1	sseq12d	$$⊢A=B\to \left(A\circ A\subseteq A\leftrightarrow B\circ B\subseteq B\right)$$
4	3	cleq2lem	$$⊢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)$$