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

Theorem mpt2eq123dv 6359
Description: An equality deduction for the maps to notation. (Contributed by NM, 12-Sep-2011.)
Hypotheses
Ref Expression
mpt2eq123dv.1
mpt2eq123dv.2
mpt2eq123dv.3
Assertion
Ref Expression
mpt2eq123dv
Distinct variable groups:   ,   ,

Proof of Theorem mpt2eq123dv
StepHypRef Expression
1 mpt2eq123dv.1 . 2
2 mpt2eq123dv.2 . . 3
32adantr 465 . 2
4 mpt2eq123dv.3 . . 3
54adantr 465 . 2
61, 3, 5mpt2eq123dva 6358 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  =wceq 1395  e.wcel 1818  e.cmpt2 6298
This theorem is referenced by:  mpt2eq123i  6360  bropopvvv  6880  prdsval  14852  imasval  14908  imasvscaval  14935  homffval  15086  homfeq  15089  comfffval  15093  comffval  15094  comfffval2  15096  comffval2  15097  comfeq  15101  oppcval  15108  monfval  15127  sectffval  15145  invffval  15152  cofuval  15251  natfval  15315  fucval  15327  fucco  15331  coafval  15391  setcval  15404  setcco  15410  catcval  15423  catcco  15428  xpcval  15446  xpchomfval  15448  xpccofval  15451  1stfval  15460  2ndfval  15463  prfval  15468  evlfval  15486  evlf2  15487  curfval  15492  hofval  15521  hof2fval  15524  plusffval  15877  grpsubfval  16092  grpsubpropd  16140  mulgfval  16143  mulgpropd  16175  symgval  16404  lsmfval  16658  pj1fval  16712  efgtf  16740  prdsmgp  17259  dvrfval  17333  scaffval  17530  psrval  18011  ipffval  18683  frlmip  18809  mamufval  18887  mvmulfval  19044  marrepfval  19062  marepvfval  19067  submafval  19081  submaval  19083  madufval  19139  minmar1fval  19148  mat2pmatfval  19224  cpm2mfval  19250  decpmatval0  19265  decpmatval  19266  pmatcollpw3lem  19284  xkoval  20088  xkopt  20156  xpstopnlem1  20310  submtmd  20603  blfvalps  20886  ishtpy  21472  isphtpy  21481  pcofval  21510  rrxip  21822  q1pval  22554  r1pval  22557  taylfval  22754  midf  24142  ismidb  24144  ttgval  24178  wlkon  24533  trlon  24542  pthon  24577  spthon  24584  is2wlkonot  24863  is2spthonot  24864  2wlkonot3v  24875  2spthonot3v  24876  grpodivfval  25244  gxfval  25259  dipfval  25612  qqhval  27955  sxval  28161  sitmval  28290  cndprobval  28372  mclsval  28923  rrnval  30323  eldiophb  30690  mendval  31132  isofn  32567  estrcval  32630  estrcco  32636  rngcvalOLD  32769  rngccoOLD  32796  funcrngcsetcALT  32807  ringcvalOLD  32815  ringccoOLD  32859  lincop  33009  ldualset  34850  paddfval  35521  tgrpfset  36470  tgrpset  36471  erngfset  36525  erngset  36526  erngfset-rN  36533  erngset-rN  36534  dvafset  36730  dvaset  36731  dvhfset  36807  dvhset  36808  djaffvalN  36860  djafvalN  36861  djhffval  37123  djhfval  37124  hlhilset  37664
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-oprab 6300  df-mpt2 6301
  Copyright terms: Public domain W3C validator