# Metamath Proof Explorer

## Definition df-mpo

Description: Define maps-to notation for defining an operation via a rule. Read as "the operation defined by the map from x , y (in A X. B ) to C ( x , y ) ". An extension of df-mpt for two arguments. (Contributed by NM, 17-Feb-2008)

Ref Expression
Assertion 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\}$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 vx ${setvar}{x}$
1 cA ${class}{A}$
2 vy ${setvar}{y}$
3 cB ${class}{B}$
4 cC ${class}{C}$
5 0 2 1 3 4 cmpo ${class}\left({x}\in {A},{y}\in {B}⟼{C}\right)$
6 vz ${setvar}{z}$
7 0 cv ${setvar}{x}$
8 7 1 wcel ${wff}{x}\in {A}$
9 2 cv ${setvar}{y}$
10 9 3 wcel ${wff}{y}\in {B}$
11 8 10 wa ${wff}\left({x}\in {A}\wedge {y}\in {B}\right)$
12 6 cv ${setvar}{z}$
13 12 4 wceq ${wff}{z}={C}$
14 11 13 wa ${wff}\left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge {z}={C}\right)$
15 14 0 2 6 coprab ${class}\left\{⟨⟨{x},{y}⟩,{z}⟩|\left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge {z}={C}\right)\right\}$
16 5 15 wceq ${wff}\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\}$