Definition df-mpo 7161

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

This definition is referenced by:  mpoeq123  7226  mpoeq123dva  7228  mpoeq3dva  7231  nfmpo1  7234  nfmpo2  7235  nfmpo  7236  0mpo0  7237  mpo0  7239  cbvmpox  7247  mpov  7264  mpomptx  7265  resmpo  7272  mpofun  7276  mpo2eqb  7283  rnmpo  7284  reldmmpo  7285  elrnmpores  7288  ovmpt4g  7297  mpondm0  7386  elmpocl  7387  fmpox  7765  bropopvvv  7785  bropfvvvv  7787  tposmpo  7929  erovlem  8393  xpcomco  8607  omxpenlem  8618  cpnnen  15582  mpomptxf  30425  df1stres  30439  df2ndres  30440  f1od2  30457  sxbrsigalem5  31546  dmscut  33272  bj-dfmpoa  34413  csbmpo123  34615  uncf  34886  unccur  34890  mpobi123f  35455  cbvmpo2  41412  cbvmpo1  41413  mpomptx2  44432  cbvmpox2  44433