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

This definition is referenced by:  mpoeq123  7462  mpoeq123dva  7464  mpoeq3dva  7467  nfmpo1  7470  nfmpo2  7471  nfmpo  7472  0mpo0  7473  mpo0  7475  cbvmpox  7483  cbvmpov  7485  mpov  7502  mpomptx  7503  resmpo  7510  mpofun  7514  mpo2eqb  7522  rnmpo  7523  reldmmpo  7524  elrnmpores  7528  ovmpt4g  7537  mpondm0  7630  elmpocl  7631  fmpox  8042  bropopvvv  8062  bropfvvvv  8064  tposmpo  8236  erovlem  8788  xpcomco  9033  omxpenlem  9044  mpoaddf  11162  mpomulf  11163  cpnnen  16242  dmcuts  27859  mpomptxf  32828  df1stres  32854  df2ndres  32855  f1od2  32869  sxbrsigalem5  34544  cbvmpovw2  36555  cbvmpo1vw2  36556  cbvmpo2vw2  36557  cbvmpodavw2  36604  cbvmpo1davw2  36605  cbvmpo2davw2  36606  bj-dfmpoa  37561  csbmpo123  37778  uncf  38051  unccur  38055  mpobi123f  38614  cbvmpo2  45628  cbvmpo1  45629  mpomptx2  48910  cbvmpox2  48911  sectpropdlem  49610  invpropdlem  49612  isopropdlem  49614