Definition df-mpo 7436

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

This definition is referenced by:  mpoeq123  7505  mpoeq123dva  7507  mpoeq3dva  7510  nfmpo1  7513  nfmpo2  7514  nfmpo  7515  0mpo0  7516  mpo0  7518  cbvmpox  7526  cbvmpov  7528  mpov  7545  mpomptx  7546  resmpo  7553  mpofun  7557  mpo2eqb  7565  rnmpo  7566  reldmmpo  7567  elrnmpores  7571  ovmpt4g  7580  mpondm0  7673  elmpocl  7674  fmpox  8092  bropopvvv  8115  bropfvvvv  8117  tposmpo  8288  erovlem  8853  xpcomco  9102  omxpenlem  9113  mpoaddf  11249  mpomulf  11250  cpnnen  16265  dmscut  27856  mpomptxf  32687  df1stres  32713  df2ndres  32714  f1od2  32732  sxbrsigalem5  34290  cbvmpovw2  36243  cbvmpo1vw2  36244  cbvmpo2vw2  36245  cbvmpodavw2  36292  cbvmpo1davw2  36293  cbvmpo2davw2  36294  bj-dfmpoa  37119  csbmpo123  37332  uncf  37606  unccur  37610  mpobi123f  38169  cbvmpo2  45102  cbvmpo1  45103  mpomptx2  48251  cbvmpox2  48252