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

Definition df-mpo 5847
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 4045 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 5844 . 2 class (𝑥𝐴, 𝑦𝐵𝐶)
71cv 1342 . . . . . 6 class 𝑥
87, 3wcel 2136 . . . . 5 wff 𝑥𝐴
92cv 1342 . . . . . 6 class 𝑦
109, 4wcel 2136 . . . . 5 wff 𝑦𝐵
118, 10wa 103 . . . 4 wff (𝑥𝐴𝑦𝐵)
12 vz . . . . . 6 setvar 𝑧
1312cv 1342 . . . . 5 class 𝑧
1413, 5wceq 1343 . . . 4 wff 𝑧 = 𝐶
1511, 14wa 103 . . 3 wff ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)
1615, 1, 2, 12coprab 5843 . 2 class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
176, 16wceq 1343 1 wff (𝑥𝐴, 𝑦𝐵𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
Colors of variables: wff set class
This definition is referenced by:  mpoeq123  5901  mpoeq123dva  5903  mpoeq3dva  5906  nfmpo1  5909  nfmpo2  5910  nfmpo  5911  mpo0  5912  cbvmpox  5920  mpov  5932  mpomptx  5933  resmpo  5940  mpofun  5944  mpo2eqb  5951  rnmpo  5952  reldmmpo  5953  ovmpt4g  5964  elmpocl  6036  fmpox  6168  f1od2  6203  tposmpo  6249  erovlem  6593  xpcomco  6792  dfplpq2  7295  dfmpq2  7296
  Copyright terms: Public domain W3C validator