Definition df-mpo 7425

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 5187 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 7422	. 2 class (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)
7	1	cv 1569	. . . . . 6 class 𝑥
8	7, 3	wcel 2145	. . . . 5 wff 𝑥 ∈ 𝐴
9	2	cv 1569	. . . . . 6 class 𝑦
10	9, 4	wcel 2145	. . . . 5 wff 𝑦 ∈ 𝐵
11	8, 10	wa 401	. . . 4 wff (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)
12		vz	. . . . . 6 setvar 𝑧
13	12	cv 1569	. . . . 5 class 𝑧
14	13, 5	wceq 1570	. . . 4 wff 𝑧 = 𝐶
15	11, 14	wa 401	. . 3 wff ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)
16	15, 1, 2, 12	coprab 7421	. 2 class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
17	6, 16	wceq 1570	1 wff (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}

This definition is used by:  mpoeq123  7492  mpoeq123dva  7494  mpoeq3dva  7497  nfmpo1  7500  nfmpo2  7501  nfmpo  7502  0mpo0  7503  mpo0  7505  cbvmpox  7513  cbvmpov  7515  mpov  7532  mpomptx  7533  resmpo  7540  mpofun  7544  mpo2eqb  7552  rnmpo  7553  reldmmpo  7554  elrnmpores  7558  ovmpt4g  7567  mpondm0  7661  elmpocl  7662  fmpox  8078  bropopvvv  8101  bropfvvvv  8103  tposmpo  8280  erovlem  8834  uncf  8891  xpcomco  9086  omxpenlem  9097  mpoaddf  11294  mpomulf  11295  cpnnen  16397  dmcuts  28177  mpomptxf  33272  df1stres  33297  df2ndres  33298  f1od2  33311  sxbrsigalem5  34920  cbvmpovw2  37031  cbvmpo1vw2  37032  cbvmpo2vw2  37033  cbvmpodavw2  37080  cbvmpo1davw2  37081  cbvmpo2davw2  37082  bj-dfmpoa  38039  csbmpo123  38254  unccur  38526  mpobi123f  39094  cbvmpo2  46111  cbvmpo1  46112  mpomptx2  49446  cbvmpox2  49447  sectpropdlem  50143  invpropdlem  50145  isopropdlem  50147