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 6531
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 4639 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 6528 . 2 class (𝑥𝐴, 𝑦𝐵𝐶)
71cv 1473 . . . . . 6 class 𝑥
87, 3wcel 1976 . . . . 5 wff 𝑥𝐴
92cv 1473 . . . . . 6 class 𝑦
109, 4wcel 1976 . . . . 5 wff 𝑦𝐵
118, 10wa 382 . . . 4 wff (𝑥𝐴𝑦𝐵)
12 vz . . . . . 6 setvar 𝑧
1312cv 1473 . . . . 5 class 𝑧
1413, 5wceq 1474 . . . 4 wff 𝑧 = 𝐶
1511, 14wa 382 . . 3 wff ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)
1615, 1, 2, 12coprab 6527 . 2 class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
176, 16wceq 1474 1 wff (𝑥𝐴, 𝑦𝐵𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
Colors of variables: wff setvar class
This definition is referenced by:  mpt2eq123  6589  mpt2eq123dva  6591  mpt2eq3dva  6594  nfmpt21  6597  nfmpt22  6598  nfmpt2  6599  mpt20  6600  cbvmpt2x  6608  mpt2v  6625  mpt2mptx  6626  resmpt2  6633  mpt2fun  6637  mpt22eqb  6644  rnmpt2  6645  reldmmpt2  6646  elrnmpt2res  6649  ovmpt4g  6658  mpt2ndm0  6750  elmpt2cl  6751  fmpt2x  7102  bropopvvv  7119  bropfvvvv  7121  tposmpt2  7253  erovlem  7707  xpcomco  7912  omxpenlem  7923  cpnnen  14745  2wlkonot3v  26195  2spthonot3v  26196  mpt2mptxf  28653  df1stres  28657  df2ndres  28658  f1od2  28680  sxbrsigalem5  29470  bj-dfmpt2a  32035  csbmpt22g  32136  uncf  32341  unccur  32345  mpt2bi123f  32924  cbvmpt22  38088  cbvmpt21  38089  mpt2mptx2  41887  cbvmpt2x2  41888
  Copyright terms: Public domain W3C validator