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

Definition df-mpt2 5495
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 3817 for two arguments. (Contributed by NM, 17-Feb-2008.)
Assertion
Ref Expression
df-mpt2 (𝑥𝐴, 𝑦𝐵𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
Distinct variable groups:   𝑥,𝑧   𝑦,𝑧   𝑧,𝐴   𝑧,𝐵   𝑧,𝐶
Allowed substitution hints:   𝐴(𝑥,𝑦)   𝐵(𝑥,𝑦)   𝐶(𝑥,𝑦)

Detailed syntax breakdown of Definition df-mpt2
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, 5cmpt2 5492 . 2 class (𝑥𝐴, 𝑦𝐵𝐶)
71cv 1242 . . . . . 6 class 𝑥
87, 3wcel 1393 . . . . 5 wff 𝑥𝐴
92cv 1242 . . . . . 6 class 𝑦
109, 4wcel 1393 . . . . 5 wff 𝑦𝐵
118, 10wa 97 . . . 4 wff (𝑥𝐴𝑦𝐵)
12 vz . . . . . 6 setvar 𝑧
1312cv 1242 . . . . 5 class 𝑧
1413, 5wceq 1243 . . . 4 wff 𝑧 = 𝐶
1511, 14wa 97 . . 3 wff ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)
1615, 1, 2, 12coprab 5491 . 2 class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
176, 16wceq 1243 1 wff (𝑥𝐴, 𝑦𝐵𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
Colors of variables: wff set class
This definition is referenced by:  mpt2eq123  5542  mpt2eq123dva  5544  mpt2eq3dva  5547  nfmpt21  5549  nfmpt22  5550  nfmpt2  5551  mpt20  5552  cbvmpt2x  5560  mpt2v  5572  mpt2mptx  5573  resmpt2  5577  mpt2fun  5581  mpt22eqb  5588  rnmpt2  5589  reldmmpt2  5590  ovmpt4g  5601  elmpt2cl  5676  fmpt2x  5804  tposmpt2  5874  erovlem  6176  xpcomco  6278  dfplpq2  6424  dfmpq2  6425
  Copyright terms: Public domain W3C validator