Definition df-mpo 7415

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

This definition is referenced by:  mpoeq123  7482  mpoeq123dva  7484  mpoeq3dva  7487  nfmpo1  7490  nfmpo2  7491  nfmpo  7492  0mpo0  7493  mpo0  7495  cbvmpox  7503  cbvmpov  7505  mpov  7522  mpomptx  7523  resmpo  7530  mpofun  7534  mpo2eqb  7542  rnmpo  7543  reldmmpo  7544  elrnmpores  7548  ovmpt4g  7557  mpondm0  7650  elmpocl  7651  fmpox  8063  bropopvvv  8084  bropfvvvv  8086  tposmpo  8258  erovlem  8810  xpcomco  9054  omxpenlem  9065  mpoaddf  11193  mpomulf  11194  cpnnen  16284  dmcuts  27960  mpomptxf  32989  df1stres  33015  df2ndres  33016  f1od2  33030  sxbrsigalem5  34644  cbvmpovw2  36720  cbvmpo1vw2  36721  cbvmpo2vw2  36722  cbvmpodavw2  36769  cbvmpo1davw2  36770  cbvmpo2davw2  36771  bj-dfmpoa  37726  csbmpo123  37943  uncf  38216  unccur  38220  mpobi123f  38779  cbvmpo2  45785  cbvmpo1  45786  mpomptx2  49082  cbvmpox2  49083  sectpropdlem  49781  invpropdlem  49783  isopropdlem  49785