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

Definition df-mpt2 6179
Description: Define maps-to notation for defining an operation via a rule. Read as "the operation defined by the map from x, (in X. ) to (x, )." An extension of df-mpt 4434 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 6176 . 2
71cv 1369 . . . . . 6
87, 3wcel 1757 . . . . 5
92cv 1369 . . . . . 6
109, 4wcel 1757 . . . . 5
118, 10wa 369 . . . 4
12 vz . . . . . 6
1312cv 1369 . . . . 5
1413, 5wceq 1370 . . . 4
1511, 14wa 369 . . 3
1615, 1, 2, 12coprab 6175 . 2
176, 16wceq 1370 1
Colors of variables: wff setvar class
This definition is referenced by:  mpt2eq123  6228  mpt2eq123dva  6230  mpt2eq3dva  6233  nfmpt21  6236  nfmpt22  6237  nfmpt2  6238  mpt20  6239  cbvmpt2x  6247  mpt2v  6264  mpt2mptx  6265  resmpt2  6272  mpt2fun  6276  mpt22eqb  6283  rnmpt2  6284  reldmmpt2  6285  elrnmpt2res  6288  ovmpt4g  6297  elmpt2cl  6388  fmpt2x  6724  bropopvvv  6737  mpt2ndm0  6823  tposmpt2  6866  erovlem  7280  xpcomco  7485  omxpenlem  7496  cpnnen  13597  mpt2mptxf  26113  df1stres  26117  df2ndres  26118  f1od2  26142  sxbrsigalem5  26821  mpt2bi123f  29097  2wlkonot3v  30516  2spthonot3v  30517  mpt2mptx2  30846  cbvmpt2x2  30848
  Copyright terms: Public domain W3C validator