# Metamath Proof Explorer

## Theorem mpoeq123dva

Description: An equality deduction for the maps-to notation. (Contributed by Mario Carneiro, 26-Jan-2017)

Ref Expression
Hypotheses mpoeq123dv.1 ${⊢}{\phi }\to {A}={D}$
mpoeq123dva.2 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}={E}$
mpoeq123dva.3 ${⊢}\left({\phi }\wedge \left({x}\in {A}\wedge {y}\in {B}\right)\right)\to {C}={F}$
Assertion mpoeq123dva ${⊢}{\phi }\to \left({x}\in {A},{y}\in {B}⟼{C}\right)=\left({x}\in {D},{y}\in {E}⟼{F}\right)$

### Proof

Step Hyp Ref Expression
1 mpoeq123dv.1 ${⊢}{\phi }\to {A}={D}$
2 mpoeq123dva.2 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}={E}$
3 mpoeq123dva.3 ${⊢}\left({\phi }\wedge \left({x}\in {A}\wedge {y}\in {B}\right)\right)\to {C}={F}$
4 3 eqeq2d ${⊢}\left({\phi }\wedge \left({x}\in {A}\wedge {y}\in {B}\right)\right)\to \left({z}={C}↔{z}={F}\right)$
5 4 pm5.32da ${⊢}{\phi }\to \left(\left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge {z}={C}\right)↔\left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge {z}={F}\right)\right)$
6 2 eleq2d ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \left({y}\in {B}↔{y}\in {E}\right)$
7 6 pm5.32da ${⊢}{\phi }\to \left(\left({x}\in {A}\wedge {y}\in {B}\right)↔\left({x}\in {A}\wedge {y}\in {E}\right)\right)$
8 1 eleq2d ${⊢}{\phi }\to \left({x}\in {A}↔{x}\in {D}\right)$
9 8 anbi1d ${⊢}{\phi }\to \left(\left({x}\in {A}\wedge {y}\in {E}\right)↔\left({x}\in {D}\wedge {y}\in {E}\right)\right)$
10 7 9 bitrd ${⊢}{\phi }\to \left(\left({x}\in {A}\wedge {y}\in {B}\right)↔\left({x}\in {D}\wedge {y}\in {E}\right)\right)$
11 10 anbi1d ${⊢}{\phi }\to \left(\left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge {z}={F}\right)↔\left(\left({x}\in {D}\wedge {y}\in {E}\right)\wedge {z}={F}\right)\right)$
12 5 11 bitrd ${⊢}{\phi }\to \left(\left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge {z}={C}\right)↔\left(\left({x}\in {D}\wedge {y}\in {E}\right)\wedge {z}={F}\right)\right)$
13 12 oprabbidv ${⊢}{\phi }\to \left\{⟨⟨{x},{y}⟩,{z}⟩|\left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge {z}={C}\right)\right\}=\left\{⟨⟨{x},{y}⟩,{z}⟩|\left(\left({x}\in {D}\wedge {y}\in {E}\right)\wedge {z}={F}\right)\right\}$
14 df-mpo ${⊢}\left({x}\in {A},{y}\in {B}⟼{C}\right)=\left\{⟨⟨{x},{y}⟩,{z}⟩|\left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge {z}={C}\right)\right\}$
15 df-mpo ${⊢}\left({x}\in {D},{y}\in {E}⟼{F}\right)=\left\{⟨⟨{x},{y}⟩,{z}⟩|\left(\left({x}\in {D}\wedge {y}\in {E}\right)\wedge {z}={F}\right)\right\}$
16 13 14 15 3eqtr4g ${⊢}{\phi }\to \left({x}\in {A},{y}\in {B}⟼{C}\right)=\left({x}\in {D},{y}\in {E}⟼{F}\right)$