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 ⊢ A = B → A ⊆ C ∧ φ ↔ B ⊆ C ∧ φ

Proof

Step Hyp Ref Expression
1 sseq1 ⊢ A = B → A ⊆ C ↔ B ⊆ C
2 1 anbi1d ⊢ A = B → A ⊆ C ∧ φ ↔ B ⊆ C ∧ φ