Definition df-mpo 7411

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 5232 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 7408	. 2 class (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
7	1	cv 1541	. . . . . 6 class 𝑥
8	7, 3	wcel 2107	. . . . 5 wff 𝑥 ∈ 𝐴
9	2	cv 1541	. . . . . 6 class 𝑦
10	9, 4	wcel 2107	. . . . 5 wff 𝑦 ∈ 𝐵
11	8, 10	wa 397	. . . 4 wff (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)
12		vz	. . . . . 6 setvar 𝑧
13	12	cv 1541	. . . . 5 class 𝑧
14	13, 5	wceq 1542	. . . 4 wff 𝑧 = 𝐶
15	11, 14	wa 397	. . 3 wff ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)
16	15, 1, 2, 12	coprab 7407	. 2 class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
17	6, 16	wceq 1542	1 wff (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}

This definition is referenced by:  mpoeq123  7478  mpoeq123dva  7480  mpoeq3dva  7483  nfmpo1  7486  nfmpo2  7487  nfmpo  7488  0mpo0  7489  mpo0  7491  cbvmpox  7499  mpov  7517  mpomptx  7518  resmpo  7525  mpofun  7529  mpofunOLD  7530  mpo2eqb  7538  rnmpo  7539  reldmmpo  7540  elrnmpores  7543  ovmpt4g  7552  mpondm0  7644  elmpocl  7645  fmpox  8050  bropopvvv  8073  bropfvvvv  8075  tposmpo  8245  erovlem  8804  xpcomco  9059  omxpenlem  9070  cpnnen  16169  dmscut  27302  mpomptxf  31893  df1stres  31913  df2ndres  31914  f1od2  31934  sxbrsigalem5  33276  mpomulf  35148  bj-dfmpoa  35988  csbmpo123  36201  uncf  36456  unccur  36460  mpobi123f  37019  cbvmpo2  43772  cbvmpo1  43773  mpomptx2  46964  cbvmpox2  46965