Theorem cleq2lem

Description: Equality implies bijection. (Contributed by RP, 24-Jul-2020)

	Ref	Expression
Hypothesis	cleq2lem.b	⊢ ( 𝐴 = 𝐵 → ( 𝜑 ↔ 𝜓 ) )
Assertion	cleq2lem	⊢ ( 𝐴 = 𝐵 → ( ( 𝑅 ⊆ 𝐴 ∧ 𝜑 ) ↔ ( 𝑅 ⊆ 𝐵 ∧ 𝜓 ) ) )

Proof

Step	Hyp	Ref	Expression
1		cleq2lem.b	⊢ ( 𝐴 = 𝐵 → ( 𝜑 ↔ 𝜓 ) )
2		sseq2	⊢ ( 𝐴 = 𝐵 → ( 𝑅 ⊆ 𝐴 ↔ 𝑅 ⊆ 𝐵 ) )
3	2 1	anbi12d	⊢ ( 𝐴 = 𝐵 → ( ( 𝑅 ⊆ 𝐴 ∧ 𝜑 ) ↔ ( 𝑅 ⊆ 𝐵 ∧ 𝜓 ) ) )