Definition df-mpo 7395

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 5192 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 7392	. 2 class (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
7	1	cv 1539	. . . . . 6 class 𝑥
8	7, 3	wcel 2109	. . . . 5 wff 𝑥 ∈ 𝐴
9	2	cv 1539	. . . . . 6 class 𝑦
10	9, 4	wcel 2109	. . . . 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 7391	. 2 class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
17	6, 16	wceq 1540	1 wff (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}

This definition is referenced by:  mpoeq123  7464  mpoeq123dva  7466  mpoeq3dva  7469  nfmpo1  7472  nfmpo2  7473  nfmpo  7474  0mpo0  7475  mpo0  7477  cbvmpox  7485  cbvmpov  7487  mpov  7504  mpomptx  7505  resmpo  7512  mpofun  7516  mpo2eqb  7524  rnmpo  7525  reldmmpo  7526  elrnmpores  7530  ovmpt4g  7539  mpondm0  7632  elmpocl  7633  fmpox  8049  bropopvvv  8072  bropfvvvv  8074  tposmpo  8245  erovlem  8789  xpcomco  9036  omxpenlem  9047  mpoaddf  11169  mpomulf  11170  cpnnen  16204  dmscut  27730  mpomptxf  32608  df1stres  32634  df2ndres  32635  f1od2  32651  sxbrsigalem5  34286  cbvmpovw2  36237  cbvmpo1vw2  36238  cbvmpo2vw2  36239  cbvmpodavw2  36286  cbvmpo1davw2  36287  cbvmpo2davw2  36288  bj-dfmpoa  37113  csbmpo123  37326  uncf  37600  unccur  37604  mpobi123f  38163  cbvmpo2  45098  cbvmpo1  45099  mpomptx2  48327  cbvmpox2  48328  sectpropdlem  49029  invpropdlem  49031  isopropdlem  49033