Definition df-mpo 7453

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

This definition is referenced by:  mpoeq123  7522  mpoeq123dva  7524  mpoeq3dva  7527  nfmpo1  7530  nfmpo2  7531  nfmpo  7532  0mpo0  7533  mpo0  7535  cbvmpox  7543  cbvmpov  7545  mpov  7562  mpomptx  7563  resmpo  7570  mpofun  7574  mpo2eqb  7582  rnmpo  7583  reldmmpo  7584  elrnmpores  7588  ovmpt4g  7597  mpondm0  7690  elmpocl  7691  fmpox  8108  bropopvvv  8131  bropfvvvv  8133  tposmpo  8304  erovlem  8871  xpcomco  9128  omxpenlem  9139  mpoaddf  11278  mpomulf  11279  cpnnen  16277  dmscut  27874  mpomptxf  32695  df1stres  32715  df2ndres  32716  f1od2  32735  sxbrsigalem5  34253  cbvmpovw2  36208  cbvmpo1vw2  36209  cbvmpo2vw2  36210  cbvmpodavw2  36257  cbvmpo1davw2  36258  cbvmpo2davw2  36259  bj-dfmpoa  37084  csbmpo123  37297  uncf  37559  unccur  37563  mpobi123f  38122  cbvmpo2  44999  cbvmpo1  45000  mpomptx2  48059  cbvmpox2  48060