Theorem trcleq12lem

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

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

Proof

Step	Hyp	Ref	Expression
1		cleq1lem	$$⊢R=S\to \left(\left(R\subseteq A\wedge A\circ A\subseteq A\right)\leftrightarrow \left(S\subseteq A\wedge A\circ A\subseteq A\right)\right)$$
2		trcleq2lem	$$⊢A=B\to \left(\left(S\subseteq A\wedge A\circ A\subseteq A\right)\leftrightarrow \left(S\subseteq B\wedge B\circ B\subseteq B\right)\right)$$
3	1 2	sylan9bb	$$⊢\left(R=S\wedge A=B\right)\to \left(\left(R\subseteq A\wedge A\circ A\subseteq A\right)\leftrightarrow \left(S\subseteq B\wedge B\circ B\subseteq B\right)\right)$$