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

Definition df-mpo 5901
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 4081 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 5898 . 2 class (𝑥𝐴, 𝑦𝐵𝐶)
71cv 1363 . . . . . 6 class 𝑥
87, 3wcel 2160 . . . . 5 wff 𝑥𝐴
92cv 1363 . . . . . 6 class 𝑦
109, 4wcel 2160 . . . . 5 wff 𝑦𝐵
118, 10wa 104 . . . 4 wff (𝑥𝐴𝑦𝐵)
12 vz . . . . . 6 setvar 𝑧
1312cv 1363 . . . . 5 class 𝑧
1413, 5wceq 1364 . . . 4 wff 𝑧 = 𝐶
1511, 14wa 104 . . 3 wff ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)
1615, 1, 2, 12coprab 5897 . 2 class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
176, 16wceq 1364 1 wff (𝑥𝐴, 𝑦𝐵𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
Colors of variables: wff set class
This definition is referenced by:  mpoeq123  5955  mpoeq123dva  5957  mpoeq3dva  5960  nfmpo1  5963  nfmpo2  5964  nfmpo  5965  mpo0  5966  cbvmpox  5974  mpov  5986  mpomptx  5987  resmpo  5994  mpofun  5998  mpo2eqb  6006  rnmpo  6007  reldmmpo  6008  ovmpt4g  6019  elmpocl  6091  fmpox  6225  f1od2  6260  tposmpo  6306  erovlem  6653  xpcomco  6852  dfplpq2  7383  dfmpq2  7384
  Copyright terms: Public domain W3C validator