Definition df-mpo 7448

Description: Define maps-to notation for defining an operation via a rule. Read as "the operation defined by the map from 𝑥, 𝑦 (in 𝐴 × 𝐵) to 𝐶(𝑥, 𝑦)". An extension of df-mpt 5190 for two arguments. (Contributed by NM, 17-Feb-2008.)

Assertion

Ref	Expression
df-mpo	⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}

Distinct variable groups:   𝑥,𝑧   𝑦,𝑧   𝑧,𝐴   𝑧,𝐵   𝑧,𝐶

Allowed substitution hints:   𝐴(𝑥, 𝑦)   𝐵(𝑥, 𝑦)   𝐶(𝑥, 𝑦)

Detailed syntax breakdown of Definition df-mpo

Step	Hyp	Ref	Expression
1		vx	. . 3 setvar 𝑥
2		vy	. . 3 setvar 𝑦
3		cA	. . 3 class 𝐴
4		cB	. . 3 class 𝐵
5		cC	. . 3 class 𝐶
6	1, 2, 3, 4, 5	cmpo 7445	. 2 class (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
7	1	cv 1569	. . . . . 6 class 𝑥
8	7, 3	wcel 2147	. . . . 5 wff 𝑥 ∈ 𝐴
9	2	cv 1569	. . . . . 6 class 𝑦
10	9, 4	wcel 2147	. . . . 5 wff 𝑦 ∈ 𝐵
11	8, 10	wa 401	. . . 4 wff (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)
12		vz	. . . . . 6 setvar 𝑧
13	12	cv 1569	. . . . 5 class 𝑧
14	13, 5	wceq 1570	. . . 4 wff 𝑧 = 𝐶
15	11, 14	wa 401	. . 3 wff ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)
16	15, 1, 2, 12	coprab 7444	. 2 class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
17	6, 16	wceq 1570	1 wff (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}

This definition is used by:  mpoeq123  7515  mpoeq123dva  7517  mpoeq3dva  7520  nfmpo1  7523  nfmpo2  7524  nfmpo  7525  0mpo0  7526  mpo0  7528  cbvmpox  7536  cbvmpov  7538  mpov  7555  mpomptx  7556  resmpo  7563  mpofun  7567  mpo2eqb  7575  reldmmpo  7576  rnmpo  7577  elrnmpores  7582  ovmpt4g  7591  mpondm0  7685  elmpocl  7686  fmpox  8103  bropopvvv  8126  bropfvvvv  8128  f1od2  8135  tposmpo  8308  erovlem  8862  uncf  8919  xpcomco  9114  omxpenlem  9125  mpoaddf  11321  mpomulf  11322  cpnnen  16426  dmcuts  28207  mpomptxf  33343  df1stres  33368  df2ndres  33369  sxbrsigalem5  34990  mpofvd  35797  cbvmpovw2  37209  cbvmpo1vw2  37210  cbvmpo2vw2  37211  cbvmpodavw2  37258  cbvmpo1davw2  37259  cbvmpo2davw2  37260  bj-dfmpoa  38231  csbmpo123  38446  unccur  38718  mpobi123f  39286  cbvmpo2  46317  cbvmpo1  46318  mpomptx2  49652  cbvmpox2  49653  elovmpoeq  50185  sectpropdlem  50355  invpropdlem  50357  isopropdlem  50359