This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝐴 = 𝐵 → ( ( 𝐴 ⊆ 𝐶 ∧ 𝜑 ) ↔ ( 𝐵 ⊆ 𝐶 ∧ 𝜑 ) ) )