# Metamath Proof Explorer

## Theorem resmpo

Description: Restriction of the mapping operation. (Contributed by Mario Carneiro, 17-Dec-2013)

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

### Proof

Step Hyp Ref Expression
1 resoprab2 ${⊢}\left({C}\subseteq {A}\wedge {D}\subseteq {B}\right)\to {\left\{⟨⟨{x},{y}⟩,{z}⟩|\left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge {z}={E}\right)\right\}↾}_{\left({C}×{D}\right)}=\left\{⟨⟨{x},{y}⟩,{z}⟩|\left(\left({x}\in {C}\wedge {y}\in {D}\right)\wedge {z}={E}\right)\right\}$
2 df-mpo ${⊢}\left({x}\in {A},{y}\in {B}⟼{E}\right)=\left\{⟨⟨{x},{y}⟩,{z}⟩|\left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge {z}={E}\right)\right\}$
3 2 reseq1i ${⊢}{\left({x}\in {A},{y}\in {B}⟼{E}\right)↾}_{\left({C}×{D}\right)}={\left\{⟨⟨{x},{y}⟩,{z}⟩|\left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge {z}={E}\right)\right\}↾}_{\left({C}×{D}\right)}$
4 df-mpo ${⊢}\left({x}\in {C},{y}\in {D}⟼{E}\right)=\left\{⟨⟨{x},{y}⟩,{z}⟩|\left(\left({x}\in {C}\wedge {y}\in {D}\right)\wedge {z}={E}\right)\right\}$
5 1 3 4 3eqtr4g ${⊢}\left({C}\subseteq {A}\wedge {D}\subseteq {B}\right)\to {\left({x}\in {A},{y}\in {B}⟼{E}\right)↾}_{\left({C}×{D}\right)}=\left({x}\in {C},{y}\in {D}⟼{E}\right)$