Definition df-mpo 7408

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 5202 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 7405	. 2 class (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
7	1	cv 1539	. . . . . 6 class 𝑥
8	7, 3	wcel 2108	. . . . 5 wff 𝑥 ∈ 𝐴
9	2	cv 1539	. . . . . 6 class 𝑦
10	9, 4	wcel 2108	. . . . 5 wff 𝑦 ∈ 𝐵
11	8, 10	wa 395	. . . 4 wff (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)
12		vz	. . . . . 6 setvar 𝑧
13	12	cv 1539	. . . . 5 class 𝑧
14	13, 5	wceq 1540	. . . 4 wff 𝑧 = 𝐶
15	11, 14	wa 395	. . 3 wff ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)
16	15, 1, 2, 12	coprab 7404	. 2 class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
17	6, 16	wceq 1540	1 wff (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}

This definition is referenced by:  mpoeq123  7477  mpoeq123dva  7479  mpoeq3dva  7482  nfmpo1  7485  nfmpo2  7486  nfmpo  7487  0mpo0  7488  mpo0  7490  cbvmpox  7498  cbvmpov  7500  mpov  7517  mpomptx  7518  resmpo  7525  mpofun  7529  mpo2eqb  7537  rnmpo  7538  reldmmpo  7539  elrnmpores  7543  ovmpt4g  7552  mpondm0  7645  elmpocl  7646  fmpox  8064  bropopvvv  8087  bropfvvvv  8089  tposmpo  8260  erovlem  8825  xpcomco  9074  omxpenlem  9085  mpoaddf  11221  mpomulf  11222  cpnnen  16245  dmscut  27773  mpomptxf  32601  df1stres  32627  df2ndres  32628  f1od2  32644  sxbrsigalem5  34266  cbvmpovw2  36206  cbvmpo1vw2  36207  cbvmpo2vw2  36208  cbvmpodavw2  36255  cbvmpo1davw2  36256  cbvmpo2davw2  36257  bj-dfmpoa  37082  csbmpo123  37295  uncf  37569  unccur  37573  mpobi123f  38132  cbvmpo2  45069  cbvmpo1  45070  mpomptx2  48258  cbvmpox2  48259  sectpropdlem  48951  invpropdlem  48953  isopropdlem  48955