Definition df-mpo 7422

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 5191 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 7419	. 2 class (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
7	1	cv 1569	. . . . . 6 class 𝑥
8	7, 3	wcel 2145	. . . . 5 wff 𝑥 ∈ 𝐴
9	2	cv 1569	. . . . . 6 class 𝑦
10	9, 4	wcel 2145	. . . . 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 7418	. 2 class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
17	6, 16	wceq 1570	1 wff (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}

This definition is used by:  mpoeq123  7489  mpoeq123dva  7491  mpoeq3dva  7494  nfmpo1  7497  nfmpo2  7498  nfmpo  7499  0mpo0  7500  mpo0  7502  cbvmpox  7510  cbvmpov  7512  mpov  7529  mpomptx  7530  resmpo  7537  mpofun  7541  mpo2eqb  7549  rnmpo  7550  reldmmpo  7551  elrnmpores  7555  ovmpt4g  7564  mpondm0  7658  elmpocl  7659  fmpox  8068  bropopvvv  8091  bropfvvvv  8093  tposmpo  8265  erovlem  8817  uncf  8874  xpcomco  9069  omxpenlem  9080  mpoaddf  11222  mpomulf  11223  cpnnen  16323  dmcuts  28064  mpomptxf  33159  df1stres  33184  df2ndres  33185  f1od2  33198  sxbrsigalem5  34807  cbvmpovw2  36870  cbvmpo1vw2  36871  cbvmpo2vw2  36872  cbvmpodavw2  36919  cbvmpo1davw2  36920  cbvmpo2davw2  36921  bj-dfmpoa  37876  csbmpo123  38093  unccur  38365  mpobi123f  38918  cbvmpo2  45937  cbvmpo1  45938  mpomptx2  49273  cbvmpox2  49274  sectpropdlem  49970  invpropdlem  49972  isopropdlem  49974