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

Definition df-mpt2 6066
Description: Define maps-to notation for defining an operation via a rule. Read as "the operation defined by the map from , (in AX.B) to B( , )." An extension of df-mpt 4327 for two arguments. (Contributed by NM, 17-Feb-2008.)
Assertion
Ref Expression
df-mpt2
Distinct variable groups:   ,   ,   ,   ,   ,

Detailed syntax breakdown of Definition df-mpt2
StepHypRef Expression
1 vx . . 3
2 vy . . 3
3 cA . . 3
4 cB . . 3
5 cC . . 3
61, 2, 3, 4, 5cmpt2 6063 . 2
71cv 1686 . . . . . 6
87, 3wcel 1749 . . . . 5
92cv 1686 . . . . . 6
109, 4wcel 1749 . . . . 5
118, 10wa 362 . . . 4
12 vz . . . . . 6
1312cv 1686 . . . . 5
1413, 5wceq 1687 . . . 4
1511, 14wa 362 . . 3
1615, 1, 2, 12coprab 6062 . 2
176, 16wceq 1687 1
Colors of variables: wff setvar class
This definition is referenced by:  mpt2eq123  6115  mpt2eq123dva  6117  mpt2eq3dva  6120  nfmpt21  6123  nfmpt22  6124  nfmpt2  6125  mpt20  6126  cbvmpt2x  6134  mpt2v  6150  mpt2mptx  6151  resmpt2  6158  mpt2fun  6162  mpt22eqb  6169  rnmpt2  6170  reldmmpt2  6171  elrnmpt2res  6174  ovmpt4g  6183  elmpt2cl  6274  fmpt2x  6609  bropopvvv  6622  mpt2ndm0  6701  tposmpt2  6744  erovlem  7157  xpcomco  7360  omxpenlem  7371  cpnnen  13451  mpt2mptxf  25675  df1stres  25679  df2ndres  25680  f1od2  25704  sxbrsigalem5  26412  mpt2bi123f  28646  2wlkonot3v  30068  2spthonot3v  30069  mpt2mptx2  30397  cbvmpt2x2  30398
  Copyright terms: Public domain W3C validator