Definition df-mpo 7365

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

This definition is referenced by:  mpoeq123  7432  mpoeq123dva  7434  mpoeq3dva  7437  nfmpo1  7440  nfmpo2  7441  nfmpo  7442  0mpo0  7443  mpo0  7445  cbvmpox  7453  cbvmpov  7455  mpov  7472  mpomptx  7473  resmpo  7480  mpofun  7484  mpo2eqb  7492  rnmpo  7493  reldmmpo  7494  elrnmpores  7498  ovmpt4g  7507  mpondm0  7600  elmpocl  7601  fmpox  8013  bropopvvv  8034  bropfvvvv  8036  tposmpo  8207  erovlem  8754  xpcomco  8999  omxpenlem  9010  mpoaddf  11124  mpomulf  11125  cpnnen  16158  dmscut  27789  mpomptxf  32738  df1stres  32764  df2ndres  32765  f1od2  32779  sxbrsigalem5  34426  cbvmpovw2  36417  cbvmpo1vw2  36418  cbvmpo2vw2  36419  cbvmpodavw2  36466  cbvmpo1davw2  36467  cbvmpo2davw2  36468  bj-dfmpoa  37294  csbmpo123  37507  uncf  37771  unccur  37775  mpobi123f  38334  cbvmpo2  45377  cbvmpo1  45378  mpomptx2  48617  cbvmpox2  48618  sectpropdlem  49317  invpropdlem  49319  isopropdlem  49321