# Metamath Proof Explorer

## Theorem mpoeq3dva

Description: Slightly more general equality inference for the maps-to notation. (Contributed by NM, 17-Oct-2013)

Ref Expression
Hypothesis mpoeq3dva.1 ${⊢}\left({\phi }\wedge {x}\in {A}\wedge {y}\in {B}\right)\to {C}={D}$
Assertion mpoeq3dva ${⊢}{\phi }\to \left({x}\in {A},{y}\in {B}⟼{C}\right)=\left({x}\in {A},{y}\in {B}⟼{D}\right)$

### Proof

Step Hyp Ref Expression
1 mpoeq3dva.1 ${⊢}\left({\phi }\wedge {x}\in {A}\wedge {y}\in {B}\right)\to {C}={D}$
2 1 3expb ${⊢}\left({\phi }\wedge \left({x}\in {A}\wedge {y}\in {B}\right)\right)\to {C}={D}$
3 2 eqeq2d ${⊢}\left({\phi }\wedge \left({x}\in {A}\wedge {y}\in {B}\right)\right)\to \left({z}={C}↔{z}={D}\right)$
4 3 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}={D}\right)\right)$
5 4 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 {A}\wedge {y}\in {B}\right)\wedge {z}={D}\right)\right\}$
6 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\}$
7 df-mpo ${⊢}\left({x}\in {A},{y}\in {B}⟼{D}\right)=\left\{⟨⟨{x},{y}⟩,{z}⟩|\left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge {z}={D}\right)\right\}$
8 5 6 7 3eqtr4g ${⊢}{\phi }\to \left({x}\in {A},{y}\in {B}⟼{C}\right)=\left({x}\in {A},{y}\in {B}⟼{D}\right)$