Theorem cleq1lem

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

	Ref	Expression
Assertion	cleq1lem	⊢ ( 𝐴 = 𝐵 → ( ( 𝐴 ⊆ 𝐶 ∧ 𝜑 ) ↔ ( 𝐵 ⊆ 𝐶 ∧ 𝜑 ) ) )

Proof

Step	Hyp	Ref	Expression
1		sseq1	⊢ ( 𝐴 = 𝐵 → ( 𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶 ) )
2	1	anbi1d	⊢ ( 𝐴 = 𝐵 → ( ( 𝐴 ⊆ 𝐶 ∧ 𝜑 ) ↔ ( 𝐵 ⊆ 𝐶 ∧ 𝜑 ) ) )