Definition df-mpo 7021

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

This definition is referenced by:  mpoeq123  7084  mpoeq123dva  7086  mpoeq3dva  7089  nfmpo1  7092  nfmpo2  7093  nfmpo  7094  mpo0  7095  cbvmpox  7103  mpov  7120  mpomptx  7121  resmpo  7128  mpofun  7132  mpo2eqb  7139  rnmpo  7140  reldmmpo  7141  elrnmpores  7144  ovmpt4g  7153  mpondm0  7245  elmpocl  7246  fmpox  7621  bropopvvv  7641  bropfvvvv  7643  tposmpo  7780  erovlem  8243  xpcomco  8454  omxpenlem  8465  cpnnen  15415  mpomptxf  30115  df1stres  30127  df2ndres  30128  f1od2  30145  sxbrsigalem5  31163  dmscut  32881  bj-dfmpoa  34008  csbmpo123  34143  uncf  34402  unccur  34406  mpobi123f  34972  cbvmpo2  40902  cbvmpo1  40903  mpomptx2  43861  cbvmpox2  43862