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

Metamath Proof Explorer

Theorem mpoeq123i

Description: An equality inference for the maps-to notation. (Contributed by NM, 15-Jul-2013)

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

Proof

Step Hyp Ref Expression
1 mpoeq123i.1 ⊢ A = D
2 mpoeq123i.2 ⊢ B = E
3 mpoeq123i.3 ⊢ C = F
4 1 a1i ⊢ ⊤ → A = D
5 2 a1i ⊢ ⊤ → B = E
6 3 a1i ⊢ ⊤ → C = F
7 4 5 6 mpoeq123dv ⊢ ⊤ → x ∈ A , y ∈ B ⟼ C = x ∈ D , y ∈ E ⟼ F
8 7 mptru ⊢ x ∈ A , y ∈ B ⟼ C = x ∈ D , y ∈ E ⟼ F