Theorem trcleq12lem

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

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

Proof

Step	Hyp	Ref	Expression
1		cleq1lem	⊢ ( 𝑅 = 𝑆 → ( ( 𝑅 ⊆ 𝐴 ∧ ( 𝐴 ∘ 𝐴 ) ⊆ 𝐴 ) ↔ ( 𝑆 ⊆ 𝐴 ∧ ( 𝐴 ∘ 𝐴 ) ⊆ 𝐴 ) ) )
2		trcleq2lem	⊢ ( 𝐴 = 𝐵 → ( ( 𝑆 ⊆ 𝐴 ∧ ( 𝐴 ∘ 𝐴 ) ⊆ 𝐴 ) ↔ ( 𝑆 ⊆ 𝐵 ∧ ( 𝐵 ∘ 𝐵 ) ⊆ 𝐵 ) ) )
3	1 2	sylan9bb	⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ) → ( ( 𝑅 ⊆ 𝐴 ∧ ( 𝐴 ∘ 𝐴 ) ⊆ 𝐴 ) ↔ ( 𝑆 ⊆ 𝐵 ∧ ( 𝐵 ∘ 𝐵 ) ⊆ 𝐵 ) ) )