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

Definition df-mpo 5731
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 3949 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 5728 . 2 class (𝑥𝐴, 𝑦𝐵𝐶)
71cv 1311 . . . . . 6 class 𝑥
87, 3wcel 1461 . . . . 5 wff 𝑥𝐴
92cv 1311 . . . . . 6 class 𝑦
109, 4wcel 1461 . . . . 5 wff 𝑦𝐵
118, 10wa 103 . . . 4 wff (𝑥𝐴𝑦𝐵)
12 vz . . . . . 6 setvar 𝑧
1312cv 1311 . . . . 5 class 𝑧
1413, 5wceq 1312 . . . 4 wff 𝑧 = 𝐶
1511, 14wa 103 . . 3 wff ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)
1615, 1, 2, 12coprab 5727 . 2 class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
176, 16wceq 1312 1 wff (𝑥𝐴, 𝑦𝐵𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
Colors of variables: wff set class
This definition is referenced by:  mpoeq123  5782  mpoeq123dva  5784  mpoeq3dva  5787  nfmpo1  5790  nfmpo2  5791  nfmpo  5792  mpo0  5793  cbvmpox  5801  mpov  5813  mpomptx  5814  resmpo  5821  mpofun  5825  mpo2eqb  5832  rnmpo  5833  reldmmpo  5834  ovmpt4g  5845  elmpocl  5920  fmpox  6050  f1od2  6084  tposmpo  6130  erovlem  6473  xpcomco  6671  dfplpq2  7104  dfmpq2  7105
  Copyright terms: Public domain W3C validator