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 6816
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 4880 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 6813 . 2 class (𝑥𝐴, 𝑦𝐵𝐶)
71cv 1629 . . . . . 6 class 𝑥
87, 3wcel 2137 . . . . 5 wff 𝑥𝐴
92cv 1629 . . . . . 6 class 𝑦
109, 4wcel 2137 . . . . 5 wff 𝑦𝐵
118, 10wa 383 . . . 4 wff (𝑥𝐴𝑦𝐵)
12 vz . . . . . 6 setvar 𝑧
1312cv 1629 . . . . 5 class 𝑧
1413, 5wceq 1630 . . . 4 wff 𝑧 = 𝐶
1511, 14wa 383 . . 3 wff ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)
1615, 1, 2, 12coprab 6812 . 2 class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
176, 16wceq 1630 1 wff (𝑥𝐴, 𝑦𝐵𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
Colors of variables: wff setvar class
This definition is referenced by:  mpt2eq123  6877  mpt2eq123dva  6879  mpt2eq3dva  6882  nfmpt21  6885  nfmpt22  6886  nfmpt2  6887  mpt20  6888  cbvmpt2x  6896  mpt2v  6913  mpt2mptx  6914  resmpt2  6921  mpt2fun  6925  mpt22eqb  6932  rnmpt2  6933  reldmmpt2  6934  elrnmpt2res  6937  ovmpt4g  6946  mpt2ndm0  7038  elmpt2cl  7039  fmpt2x  7402  bropopvvv  7421  bropfvvvv  7423  tposmpt2  7556  erovlem  8008  xpcomco  8213  omxpenlem  8224  cpnnen  15155  mpt2mptxf  29784  df1stres  29788  df2ndres  29789  f1od2  29806  sxbrsigalem5  30657  dmscut  32222  bj-dfmpt2a  33375  csbmpt22g  33486  uncf  33699  unccur  33703  mpt2bi123f  34282  cbvmpt22  39774  cbvmpt21  39775  mpt2mptx2  42621  cbvmpt2x2  42622
  Copyright terms: Public domain W3C validator