Definition df-mpo 7257

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

This definition is referenced by:  mpoeq123  7322  mpoeq123dva  7324  mpoeq3dva  7327  nfmpo1  7330  nfmpo2  7331  nfmpo  7332  0mpo0  7333  mpo0  7335  cbvmpox  7343  mpov  7361  mpomptx  7362  resmpo  7369  mpofun  7373  mpofunOLD  7374  mpo2eqb  7381  rnmpo  7382  reldmmpo  7383  elrnmpores  7386  ovmpt4g  7395  mpondm0  7485  elmpocl  7486  fmpox  7877  bropopvvv  7898  bropfvvvv  7900  tposmpo  8047  erovlem  8537  xpcomco  8779  omxpenlem  8790  cpnnen  15841  mpomptxf  30893  df1stres  30913  df2ndres  30914  f1od2  30933  sxbrsigalem5  32130  dmscut  33907  bj-dfmpoa  35192  csbmpo123  35408  uncf  35662  unccur  35666  mpobi123f  36226  cbvmpo2  42509  cbvmpo1  42510  mpomptx2  45531  cbvmpox2  45532