Definition df-mpo 7392

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 5189 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 7389	. 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 7388	. 2 class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
17	6, 16	wceq 1540	1 wff (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}

This definition is referenced by:  mpoeq123  7461  mpoeq123dva  7463  mpoeq3dva  7466  nfmpo1  7469  nfmpo2  7470  nfmpo  7471  0mpo0  7472  mpo0  7474  cbvmpox  7482  cbvmpov  7484  mpov  7501  mpomptx  7502  resmpo  7509  mpofun  7513  mpo2eqb  7521  rnmpo  7522  reldmmpo  7523  elrnmpores  7527  ovmpt4g  7536  mpondm0  7629  elmpocl  7630  fmpox  8046  bropopvvv  8069  bropfvvvv  8071  tposmpo  8242  erovlem  8786  xpcomco  9031  omxpenlem  9042  mpoaddf  11162  mpomulf  11163  cpnnen  16197  dmscut  27723  mpomptxf  32601  df1stres  32627  df2ndres  32628  f1od2  32644  sxbrsigalem5  34279  cbvmpovw2  36230  cbvmpo1vw2  36231  cbvmpo2vw2  36232  cbvmpodavw2  36279  cbvmpo1davw2  36280  cbvmpo2davw2  36281  bj-dfmpoa  37106  csbmpo123  37319  uncf  37593  unccur  37597  mpobi123f  38156  cbvmpo2  45091  cbvmpo1  45092  mpomptx2  48323  cbvmpox2  48324  sectpropdlem  49025  invpropdlem  49027  isopropdlem  49029