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 ∧ φ