Definition df-mpo 7360

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

This definition is referenced by:  mpoeq123  7427  mpoeq123dva  7429  mpoeq3dva  7432  nfmpo1  7435  nfmpo2  7436  nfmpo  7437  0mpo0  7438  mpo0  7440  cbvmpox  7448  cbvmpov  7450  mpov  7467  mpomptx  7468  resmpo  7475  mpofun  7479  mpo2eqb  7487  rnmpo  7488  reldmmpo  7489  elrnmpores  7493  ovmpt4g  7502  mpondm0  7595  elmpocl  7596  fmpox  8008  bropopvvv  8029  bropfvvvv  8031  tposmpo  8202  erovlem  8746  xpcomco  8990  omxpenlem  9001  mpoaddf  11110  mpomulf  11111  cpnnen  16148  dmscut  27762  mpomptxf  32670  df1stres  32696  df2ndres  32697  f1od2  32713  sxbrsigalem5  34312  cbvmpovw2  36297  cbvmpo1vw2  36298  cbvmpo2vw2  36299  cbvmpodavw2  36346  cbvmpo1davw2  36347  cbvmpo2davw2  36348  bj-dfmpoa  37173  csbmpo123  37386  uncf  37649  unccur  37653  mpobi123f  38212  cbvmpo2  45208  cbvmpo1  45209  mpomptx2  48449  cbvmpox2  48450  sectpropdlem  49151  invpropdlem  49153  isopropdlem  49155