Theorem trcleq2lemRP

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

	Ref	Expression
Assertion	trcleq2lemRP	⊢ ( 𝐴 = 𝐵 → ( ( 𝑅 ⊆ 𝐴 ∧ ( 𝐴 ∘ 𝐴 ) ⊆ 𝐴 ) ↔ ( 𝑅 ⊆ 𝐵 ∧ ( 𝐵 ∘ 𝐵 ) ⊆ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( 𝐴 = 𝐵 → 𝐴 = 𝐵 )
2	1 1	coeq12d	⊢ ( 𝐴 = 𝐵 → ( 𝐴 ∘ 𝐴 ) = ( 𝐵 ∘ 𝐵 ) )
3	2 1	sseq12d	⊢ ( 𝐴 = 𝐵 → ( ( 𝐴 ∘ 𝐴 ) ⊆ 𝐴 ↔ ( 𝐵 ∘ 𝐵 ) ⊆ 𝐵 ) )
4	3	cleq2lem	⊢ ( 𝐴 = 𝐵 → ( ( 𝑅 ⊆ 𝐴 ∧ ( 𝐴 ∘ 𝐴 ) ⊆ 𝐴 ) ↔ ( 𝑅 ⊆ 𝐵 ∧ ( 𝐵 ∘ 𝐵 ) ⊆ 𝐵 ) ) )