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 5186 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 1568	. . . . . 6 class 𝑥
8	7, 3	wcel 2144	. . . . 5 wff 𝑥 ∈ 𝐴
9	2	cv 1568	. . . . . 6 class 𝑦
10	9, 4	wcel 2144	. . . . 5 wff 𝑦 ∈ 𝐵
11	8, 10	wa 401	. . . 4 wff (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)
12		vz	. . . . . 6 setvar 𝑧
13	12	cv 1568	. . . . 5 class 𝑧
14	13, 5	wceq 1569	. . . 4 wff 𝑧 = 𝐶
15	11, 14	wa 401	. . 3 wff ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)
16	15, 1, 2, 12	coprab 7421	. 2 class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)}
17	6, 16	wceq 1569	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  8281  erovlem  8835  uncf  8892  xpcomco  9087  omxpenlem  9098  mpoaddf  11295  mpomulf  11296  cpnnen  16398  dmcuts  28178  mpomptxf  33315  df1stres  33340  df2ndres  33341  f1od2  33354  sxbrsigalem5  34963  cbvmpovw2  37106  cbvmpo1vw2  37107  cbvmpo2vw2  37108  cbvmpodavw2  37155  cbvmpo1davw2  37156  cbvmpo2davw2  37157  bj-dfmpoa  38115  csbmpo123  38330  unccur  38602  mpobi123f  39170  cbvmpo2  46188  cbvmpo1  46189  mpomptx2  49523  cbvmpox2  49524  sectpropdlem  50220  invpropdlem  50222  isopropdlem  50224