ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-mpo GIF version

Definition df-mpo 5858
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 4052 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 5855 . 2 class (𝑥𝐴, 𝑦𝐵𝐶)
71cv 1347 . . . . . 6 class 𝑥
87, 3wcel 2141 . . . . 5 wff 𝑥𝐴
92cv 1347 . . . . . 6 class 𝑦
109, 4wcel 2141 . . . . 5 wff 𝑦𝐵
118, 10wa 103 . . . 4 wff (𝑥𝐴𝑦𝐵)
12 vz . . . . . 6 setvar 𝑧
1312cv 1347 . . . . 5 class 𝑧
1413, 5wceq 1348 . . . 4 wff 𝑧 = 𝐶
1511, 14wa 103 . . 3 wff ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)
1615, 1, 2, 12coprab 5854 . 2 class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
176, 16wceq 1348 1 wff (𝑥𝐴, 𝑦𝐵𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
Colors of variables: wff set class
This definition is referenced by:  mpoeq123  5912  mpoeq123dva  5914  mpoeq3dva  5917  nfmpo1  5920  nfmpo2  5921  nfmpo  5922  mpo0  5923  cbvmpox  5931  mpov  5943  mpomptx  5944  resmpo  5951  mpofun  5955  mpo2eqb  5962  rnmpo  5963  reldmmpo  5964  ovmpt4g  5975  elmpocl  6047  fmpox  6179  f1od2  6214  tposmpo  6260  erovlem  6605  xpcomco  6804  dfplpq2  7316  dfmpq2  7317
  Copyright terms: Public domain W3C validator