Definition df-mpo 7346

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

This definition is referenced by:  mpoeq123  7413  mpoeq123dva  7415  mpoeq3dva  7418  nfmpo1  7421  nfmpo2  7422  nfmpo  7423  0mpo0  7424  mpo0  7426  cbvmpox  7434  cbvmpov  7436  mpov  7453  mpomptx  7454  resmpo  7461  mpofun  7465  mpo2eqb  7473  rnmpo  7474  reldmmpo  7475  elrnmpores  7479  ovmpt4g  7488  mpondm0  7581  elmpocl  7582  fmpox  7994  bropopvvv  8015  bropfvvvv  8017  tposmpo  8188  erovlem  8732  xpcomco  8975  omxpenlem  8986  mpoaddf  11092  mpomulf  11093  cpnnen  16130  dmscut  27745  mpomptxf  32649  df1stres  32675  df2ndres  32676  f1od2  32692  sxbrsigalem5  34291  cbvmpovw2  36255  cbvmpo1vw2  36256  cbvmpo2vw2  36257  cbvmpodavw2  36304  cbvmpo1davw2  36305  cbvmpo2davw2  36306  bj-dfmpoa  37131  csbmpo123  37344  uncf  37618  unccur  37622  mpobi123f  38181  cbvmpo2  45113  cbvmpo1  45114  mpomptx2  48345  cbvmpox2  48346  sectpropdlem  49047  invpropdlem  49049  isopropdlem  49051