Definition df-mpo 7373

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

This definition is referenced by:  mpoeq123  7440  mpoeq123dva  7442  mpoeq3dva  7445  nfmpo1  7448  nfmpo2  7449  nfmpo  7450  0mpo0  7451  mpo0  7453  cbvmpox  7461  cbvmpov  7463  mpov  7480  mpomptx  7481  resmpo  7488  mpofun  7492  mpo2eqb  7500  rnmpo  7501  reldmmpo  7502  elrnmpores  7506  ovmpt4g  7515  mpondm0  7608  elmpocl  7609  fmpox  8021  bropopvvv  8042  bropfvvvv  8044  tposmpo  8215  erovlem  8762  xpcomco  9007  omxpenlem  9018  mpoaddf  11132  mpomulf  11133  cpnnen  16166  dmcuts  27799  mpomptxf  32767  df1stres  32793  df2ndres  32794  f1od2  32808  sxbrsigalem5  34465  cbvmpovw2  36455  cbvmpo1vw2  36456  cbvmpo2vw2  36457  cbvmpodavw2  36504  cbvmpo1davw2  36505  cbvmpo2davw2  36506  bj-dfmpoa  37362  csbmpo123  37575  uncf  37839  unccur  37843  mpobi123f  38402  cbvmpo2  45445  cbvmpo1  45446  mpomptx2  48684  cbvmpox2  48685  sectpropdlem  49384  invpropdlem  49386  isopropdlem  49388