Theorem trcleq2lem

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

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

Proof

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