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

Definition df-mpt2 6301
Description: Define maps-to notation for defining an operation via a rule. Read as "the operation defined by the map from x, (in AX. ) to (x, )." An extension of df-mpt 4512 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 6298 . 2
71cv 1394 . . . . . 6
87, 3wcel 1818 . . . . 5
92cv 1394 . . . . . 6
109, 4wcel 1818 . . . . 5
118, 10wa 369 . . . 4
12 vz . . . . . 6
1312cv 1394 . . . . 5
1413, 5wceq 1395 . . . 4
1511, 14wa 369 . . 3
1615, 1, 2, 12coprab 6297 . 2
176, 16wceq 1395 1
Colors of variables: wff setvar class
This definition is referenced by:  mpt2eq123  6356  mpt2eq123dva  6358  mpt2eq3dva  6361  nfmpt21  6364  nfmpt22  6365  nfmpt2  6366  mpt20  6367  cbvmpt2x  6375  mpt2v  6392  mpt2mptx  6393  resmpt2  6400  mpt2fun  6404  mpt22eqb  6411  rnmpt2  6412  reldmmpt2  6413  elrnmpt2res  6416  ovmpt4g  6425  mpt2ndm0  6516  elmpt2cl  6517  fmpt2x  6866  bropopvvv  6880  tposmpt2  7011  erovlem  7426  xpcomco  7627  omxpenlem  7638  cpnnen  13962  2wlkonot3v  24875  2spthonot3v  24876  mpt2mptxf  27518  df1stres  27522  df2ndres  27523  f1od2  27547  sxbrsigalem5  28259  mpt2bi123f  30571  mpt2mptx2  32924  cbvmpt2x2  32925
  Copyright terms: Public domain W3C validator