Definition df-mpo 7405

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

This definition is referenced by:  mpoeq123  7472  mpoeq123dva  7474  mpoeq3dva  7477  nfmpo1  7480  nfmpo2  7481  nfmpo  7482  0mpo0  7483  mpo0  7485  cbvmpox  7493  cbvmpov  7495  mpov  7512  mpomptx  7513  resmpo  7520  mpofun  7524  mpo2eqb  7532  rnmpo  7533  reldmmpo  7534  elrnmpores  7538  ovmpt4g  7547  mpondm0  7640  elmpocl  7641  fmpox  8052  bropopvvv  8073  bropfvvvv  8075  tposmpo  8247  erovlem  8799  xpcomco  9043  omxpenlem  9054  mpoaddf  11182  mpomulf  11183  cpnnen  16275  dmcuts  27942  mpomptxf  32935  df1stres  32961  df2ndres  32962  f1od2  32976  sxbrsigalem5  34595  cbvmpovw2  36615  cbvmpo1vw2  36616  cbvmpo2vw2  36617  cbvmpodavw2  36664  cbvmpo1davw2  36665  cbvmpo2davw2  36666  bj-dfmpoa  37620  csbmpo123  37837  uncf  38110  unccur  38114  mpobi123f  38673  cbvmpo2  45673  cbvmpo1  45674  mpomptx2  48966  cbvmpox2  48967  sectpropdlem  49665  invpropdlem  49667  isopropdlem  49669