Definition df-mpo 7398

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

This definition is referenced by:  mpoeq123  7465  mpoeq123dva  7467  mpoeq3dva  7470  nfmpo1  7473  nfmpo2  7474  nfmpo  7475  0mpo0  7476  mpo0  7478  cbvmpox  7486  mpov  7504  mpomptx  7505  resmpo  7512  mpofun  7516  mpofunOLD  7517  mpo2eqb  7524  rnmpo  7525  reldmmpo  7526  elrnmpores  7529  ovmpt4g  7538  mpondm0  7630  elmpocl  7631  fmpox  8035  bropopvvv  8058  bropfvvvv  8060  tposmpo  8230  erovlem  8790  xpcomco  9045  omxpenlem  9056  cpnnen  16154  dmscut  27238  mpomptxf  31775  df1stres  31796  df2ndres  31797  f1od2  31817  sxbrsigalem5  33118  bj-dfmpoa  35803  csbmpo123  36016  uncf  36271  unccur  36275  mpobi123f  36835  cbvmpo2  43557  cbvmpo1  43558  mpomptx2  46658  cbvmpox2  46659