# Metamath Proof Explorer

## Theorem mpoeq12

Description: An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013)

Ref Expression
Assertion mpoeq12 ${⊢}\left({A}={C}\wedge {B}={D}\right)\to \left({x}\in {A},{y}\in {B}⟼{E}\right)=\left({x}\in {C},{y}\in {D}⟼{E}\right)$

### Proof

Step Hyp Ref Expression
1 eqid ${⊢}{E}={E}$
2 1 rgenw ${⊢}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{E}={E}$
3 2 jctr ${⊢}{B}={D}\to \left({B}={D}\wedge \forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{E}={E}\right)$
4 3 ralrimivw ${⊢}{B}={D}\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({B}={D}\wedge \forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{E}={E}\right)$
5 mpoeq123 ${⊢}\left({A}={C}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({B}={D}\wedge \forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{E}={E}\right)\right)\to \left({x}\in {A},{y}\in {B}⟼{E}\right)=\left({x}\in {C},{y}\in {D}⟼{E}\right)$
6 4 5 sylan2 ${⊢}\left({A}={C}\wedge {B}={D}\right)\to \left({x}\in {A},{y}\in {B}⟼{E}\right)=\left({x}\in {C},{y}\in {D}⟼{E}\right)$