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 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
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 7395 . 2 class (𝑥𝐴, 𝑦𝐵𝐶)
71cv 1540 . . . . . 6 class 𝑥
87, 3wcel 2106 . . . . 5 wff 𝑥𝐴
92cv 1540 . . . . . 6 class 𝑦
109, 4wcel 2106 . . . . 5 wff 𝑦𝐵
118, 10wa 396 . . . 4 wff (𝑥𝐴𝑦𝐵)
12 vz . . . . . 6 setvar 𝑧
1312cv 1540 . . . . 5 class 𝑧
1413, 5wceq 1541 . . . 4 wff 𝑧 = 𝐶
1511, 14wa 396 . . 3 wff ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)
1615, 1, 2, 12coprab 7394 . 2 class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
176, 16wceq 1541 1 wff (𝑥𝐴, 𝑦𝐵𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator