MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-mpt2 Structured version   Visualization version   GIF version

Definition df-mpt2 6554
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 4645 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 6551 . 2 class (𝑥𝐴, 𝑦𝐵𝐶)
71cv 1474 . . . . . 6 class 𝑥
87, 3wcel 1977 . . . . 5 wff 𝑥𝐴
92cv 1474 . . . . . 6 class 𝑦
109, 4wcel 1977 . . . . 5 wff 𝑦𝐵
118, 10wa 383 . . . 4 wff (𝑥𝐴𝑦𝐵)
12 vz . . . . . 6 setvar 𝑧
1312cv 1474 . . . . 5 class 𝑧
1413, 5wceq 1475 . . . 4 wff 𝑧 = 𝐶
1511, 14wa 383 . . 3 wff ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)
1615, 1, 2, 12coprab 6550 . 2 class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
176, 16wceq 1475 1 wff (𝑥𝐴, 𝑦𝐵𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
Colors of variables: wff setvar class
This definition is referenced by:  mpt2eq123  6612  mpt2eq123dva  6614  mpt2eq3dva  6617  nfmpt21  6620  nfmpt22  6621  nfmpt2  6622  mpt20  6623  cbvmpt2x  6631  mpt2v  6648  mpt2mptx  6649  resmpt2  6656  mpt2fun  6660  mpt22eqb  6667  rnmpt2  6668  reldmmpt2  6669  elrnmpt2res  6672  ovmpt4g  6681  mpt2ndm0  6773  elmpt2cl  6774  fmpt2x  7125  bropopvvv  7142  bropfvvvv  7144  tposmpt2  7276  erovlem  7730  xpcomco  7935  omxpenlem  7946  cpnnen  14797  2wlkonot3v  26402  2spthonot3v  26403  mpt2mptxf  28860  df1stres  28864  df2ndres  28865  f1od2  28887  sxbrsigalem5  29677  bj-dfmpt2a  32252  csbmpt22g  32353  uncf  32558  unccur  32562  mpt2bi123f  33141  cbvmpt22  38305  cbvmpt21  38306  mpt2mptx2  41906  cbvmpt2x2  41907
  Copyright terms: Public domain W3C validator