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

Definition df-mpo 7161
 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 5117 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 7158 . 2 class (𝑥𝐴, 𝑦𝐵𝐶)
71cv 1537 . . . . . 6 class 𝑥
87, 3wcel 2111 . . . . 5 wff 𝑥𝐴
92cv 1537 . . . . . 6 class 𝑦
109, 4wcel 2111 . . . . 5 wff 𝑦𝐵
118, 10wa 399 . . . 4 wff (𝑥𝐴𝑦𝐵)
12 vz . . . . . 6 setvar 𝑧
1312cv 1537 . . . . 5 class 𝑧
1413, 5wceq 1538 . . . 4 wff 𝑧 = 𝐶
1511, 14wa 399 . . 3 wff ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)
1615, 1, 2, 12coprab 7157 . 2 class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
176, 16wceq 1538 1 wff (𝑥𝐴, 𝑦𝐵𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
 Colors of variables: wff setvar class This definition is referenced by:  mpoeq123  7226  mpoeq123dva  7228  mpoeq3dva  7231  nfmpo1  7234  nfmpo2  7235  nfmpo  7236  0mpo0  7237  mpo0  7239  cbvmpox  7247  mpov  7264  mpomptx  7265  resmpo  7272  mpofun  7276  mpofunOLD  7277  mpo2eqb  7284  rnmpo  7285  reldmmpo  7286  elrnmpores  7289  ovmpt4g  7298  mpondm0  7388  elmpocl  7389  fmpox  7775  bropopvvv  7796  bropfvvvv  7798  tposmpo  7945  erovlem  8409  xpcomco  8641  omxpenlem  8652  cpnnen  15643  mpomptxf  30552  df1stres  30572  df2ndres  30573  f1od2  30592  sxbrsigalem5  31786  dmscut  33600  bj-dfmpoa  34847  csbmpo123  35062  uncf  35350  unccur  35354  mpobi123f  35914  cbvmpo2  42141  cbvmpo1  42142  mpomptx2  45152  cbvmpox2  45153
 Copyright terms: Public domain W3C validator