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	$$setvarx$$
1		cA	$$classA$$
2		vy	$$setvary$$
3		cB	$$classB$$
4		cC	$$classC$$
5	0 2 1 3 4	cmpo	$$class\left(x\in A,y\in B⟼C\right)$$
6		vz	$$setvarz$$
7	0	cv	$$setvarx$$
8	7 1	wcel	$$wffx\in A$$
9	2	cv	$$setvary$$
10	9 3	wcel	$$wffy\in B$$
11	8 10	wa	$$wff\left(x\in A\wedge y\in B\right)$$
12	6	cv	$$setvarz$$
13	12 4	wceq	$$wffz=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\}$$