MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-mpo Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 vx . . 3 setvar 𝑥
2 vy . . 3 setvar 𝑦
3 cA . . 3 class 𝐴
4 cB . . 3 class 𝐵
5 cC . . 3 class 𝐶
61, 2, 3, 4, 5cmpo 7433 . 2 class (𝑥𝐴, 𝑦𝐵𝐶)
71cv 1539 . . . . . 6 class 𝑥
87, 3wcel 2108 . . . . 5 wff 𝑥𝐴
92cv 1539 . . . . . 6 class 𝑦
109, 4wcel 2108 . . . . 5 wff 𝑦𝐵
118, 10wa 395 . . . 4 wff (𝑥𝐴𝑦𝐵)
12 vz . . . . . 6 setvar 𝑧
1312cv 1539 . . . . 5 class 𝑧
1413, 5wceq 1540 . . . 4 wff 𝑧 = 𝐶
1511, 14wa 395 . . 3 wff ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)
1615, 1, 2, 12coprab 7432 . 2 class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
176, 16wceq 1540 1 wff (𝑥𝐴, 𝑦𝐵𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator