Definition df-mpo 7435

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

This definition is referenced by:  mpoeq123  7504  mpoeq123dva  7506  mpoeq3dva  7509  nfmpo1  7512  nfmpo2  7513  nfmpo  7514  0mpo0  7515  mpo0  7517  cbvmpox  7525  cbvmpov  7527  mpov  7544  mpomptx  7545  resmpo  7552  mpofun  7556  mpo2eqb  7564  rnmpo  7565  reldmmpo  7566  elrnmpores  7570  ovmpt4g  7579  mpondm0  7672  elmpocl  7673  fmpox  8090  bropopvvv  8113  bropfvvvv  8115  tposmpo  8286  erovlem  8851  xpcomco  9100  omxpenlem  9111  mpoaddf  11246  mpomulf  11247  cpnnen  16261  dmscut  27870  mpomptxf  32693  df1stres  32718  df2ndres  32719  f1od2  32738  sxbrsigalem5  34269  cbvmpovw2  36224  cbvmpo1vw2  36225  cbvmpo2vw2  36226  cbvmpodavw2  36273  cbvmpo1davw2  36274  cbvmpo2davw2  36275  bj-dfmpoa  37100  csbmpo123  37313  uncf  37585  unccur  37589  mpobi123f  38148  cbvmpo2  45036  cbvmpo1  45037  mpomptx2  48179  cbvmpox2  48180