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 6875
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 4924 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 6872 . 2 class (𝑥𝐴, 𝑦𝐵𝐶)
71cv 1636 . . . . . 6 class 𝑥
87, 3wcel 2156 . . . . 5 wff 𝑥𝐴
92cv 1636 . . . . . 6 class 𝑦
109, 4wcel 2156 . . . . 5 wff 𝑦𝐵
118, 10wa 384 . . . 4 wff (𝑥𝐴𝑦𝐵)
12 vz . . . . . 6 setvar 𝑧
1312cv 1636 . . . . 5 class 𝑧
1413, 5wceq 1637 . . . 4 wff 𝑧 = 𝐶
1511, 14wa 384 . . 3 wff ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)
1615, 1, 2, 12coprab 6871 . 2 class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
176, 16wceq 1637 1 wff (𝑥𝐴, 𝑦𝐵𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐵) ∧ 𝑧 = 𝐶)}
Colors of variables: wff setvar class
This definition is referenced by:  mpt2eq123  6940  mpt2eq123dva  6942  mpt2eq3dva  6945  nfmpt21  6948  nfmpt22  6949  nfmpt2  6950  mpt20  6951  cbvmpt2x  6959  mpt2v  6976  mpt2mptx  6977  resmpt2  6984  mpt2fun  6988  mpt22eqb  6995  rnmpt2  6996  reldmmpt2  6997  elrnmpt2res  7000  ovmpt4g  7009  mpt2ndm0  7101  elmpt2cl  7102  fmpt2x  7465  bropopvvv  7485  bropfvvvv  7487  tposmpt2  7620  erovlem  8075  xpcomco  8285  omxpenlem  8296  cpnnen  15174  mpt2mptxf  29800  df1stres  29804  df2ndres  29805  f1od2  29822  sxbrsigalem5  30671  dmscut  32234  bj-dfmpt2a  33377  csbmpt22g  33489  uncf  33696  unccur  33700  mpt2bi123f  34276  cbvmpt22  39764  cbvmpt21  39765  mpt2mptx2  42675  cbvmpt2x2  42676
  Copyright terms: Public domain W3C validator