Metamath Proof Explorer

Theorem mpteq1dfOLD

Description: Obsolete version of mpteq1df as of 11-Nov-2024. (Contributed by Glauco Siliprandi, 23-Oct-2021) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses mpteq1df.1 ⊢ Ⅎ x φ
mpteq1df.2 ⊢ φ → A = B
Assertion mpteq1dfOLD ⊢ φ → x ∈ A ⟼ C = x ∈ B ⟼ C

Proof

Step Hyp Ref Expression
1 mpteq1df.1 ⊢ Ⅎ x φ
2 mpteq1df.2 ⊢ φ → A = B
3 1 2 alrimi ⊢ φ → ∀ x A = B
4 eqid ⊢ C = C
5 4 rgenw ⊢ ∀ x ∈ A C = C
6 mpteq12f ⊢ ∀ x A = B ∧ ∀ x ∈ A C = C → x ∈ A ⟼ C = x ∈ B ⟼ C
7 3 5 6 sylancl ⊢ φ → x ∈ A ⟼ C = x ∈ B ⟼ C