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

Metamath Proof Explorer

Theorem mpteq1df

Description: An equality theorem for the maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021) (Proof shortened by SN, 11-Nov-2024)

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 eqidd ⊢ φ → C = C
4 1 2 3 mpteq12df ⊢ φ → x ∈ A ⟼ C = x ∈ B ⟼ C