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

Metamath Proof Explorer

Theorem mpoeq123dv

Description: An equality deduction for the maps-to notation. (Contributed by NM, 12-Sep-2011)

Ref Expression
Hypotheses mpoeq123dv.1 ⊢ φ → A = D
mpoeq123dv.2 ⊢ φ → B = E
mpoeq123dv.3 ⊢ φ → C = F
Assertion mpoeq123dv ⊢ φ → x ∈ A , y ∈ B ⟼ C = x ∈ D , y ∈ E ⟼ F

Proof

Step Hyp Ref Expression
1 mpoeq123dv.1 ⊢ φ → A = D
2 mpoeq123dv.2 ⊢ φ → B = E
3 mpoeq123dv.3 ⊢ φ → C = F
4 2 adantr ⊢ φ ∧ x ∈ A → B = E
5 3 adantr ⊢ φ ∧ x ∈ A ∧ y ∈ B → C = F
6 1 4 5 mpoeq123dva ⊢ φ → x ∈ A , y ∈ B ⟼ C = x ∈ D , y ∈ E ⟼ F