Metamath Proof Explorer

Theorem mpteq1df

Description: An equality theorem for the maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses mpteq1df.1 ⊢ Ⅎ x φ
mpteq1df.2 ⊢ φ → A = B
Assertion mpteq1df ⊢ φ → 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