Definition df-mpo 7363

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

This definition is referenced by:  mpoeq123  7430  mpoeq123dva  7432  mpoeq3dva  7435  nfmpo1  7438  nfmpo2  7439  nfmpo  7440  0mpo0  7441  mpo0  7443  cbvmpox  7451  cbvmpov  7453  mpov  7470  mpomptx  7471  resmpo  7478  mpofun  7482  mpo2eqb  7490  rnmpo  7491  reldmmpo  7492  elrnmpores  7496  ovmpt4g  7505  mpondm0  7598  elmpocl  7599  fmpox  8011  bropopvvv  8031  bropfvvvv  8033  tposmpo  8204  erovlem  8751  xpcomco  8996  omxpenlem  9007  mpoaddf  11121  mpomulf  11122  cpnnen  16185  dmcuts  27802  mpomptxf  32771  df1stres  32797  df2ndres  32798  f1od2  32812  sxbrsigalem5  34453  cbvmpovw2  36445  cbvmpo1vw2  36446  cbvmpo2vw2  36447  cbvmpodavw2  36494  cbvmpo1davw2  36495  cbvmpo2davw2  36496  bj-dfmpoa  37443  csbmpo123  37658  uncf  37931  unccur  37935  mpobi123f  38494  cbvmpo2  45542  cbvmpo1  45543  mpomptx2  48808  cbvmpox2  48809  sectpropdlem  49508  invpropdlem  49510  isopropdlem  49512