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

Definition df-mpo 5786
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 3998 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 5783 . 2 class (𝑥𝐴, 𝑦𝐵𝐶)
71cv 1331 . . . . . 6 class 𝑥
87, 3wcel 1481 . . . . 5 wff 𝑥𝐴
92cv 1331 . . . . . 6 class 𝑦
109, 4wcel 1481 . . . . 5 wff 𝑦𝐵
118, 10wa 103 . . . 4 wff (𝑥𝐴𝑦𝐵)
12 vz . . . . . 6 setvar 𝑧
1312cv 1331 . . . . 5 class 𝑧
1413, 5wceq 1332 . . . 4 wff 𝑧 = 𝐶
1511, 14wa 103 . . 3 wff ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)
1615, 1, 2, 12coprab 5782 . 2 class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
176, 16wceq 1332 1 wff (𝑥𝐴, 𝑦𝐵𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
Colors of variables: wff set class
This definition is referenced by:  mpoeq123  5837  mpoeq123dva  5839  mpoeq3dva  5842  nfmpo1  5845  nfmpo2  5846  nfmpo  5847  mpo0  5848  cbvmpox  5856  mpov  5868  mpomptx  5869  resmpo  5876  mpofun  5880  mpo2eqb  5887  rnmpo  5888  reldmmpo  5889  ovmpt4g  5900  elmpocl  5975  fmpox  6105  f1od2  6139  tposmpo  6185  erovlem  6528  xpcomco  6727  dfplpq2  7185  dfmpq2  7186
  Copyright terms: Public domain W3C validator