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

Theorem mpt2eq3dva 6361
Description: Slightly more general equality inference for the maps to notation. (Contributed by NM, 17-Oct-2013.)
Hypothesis
Ref Expression
mpt2eq3dva.1
Assertion
Ref Expression
mpt2eq3dva
Distinct variable groups:   ,   ,

Proof of Theorem mpt2eq3dva
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 mpt2eq3dva.1 . . . . . 6
213expb 1197 . . . . 5
32eqeq2d 2471 . . . 4
43pm5.32da 641 . . 3
54oprabbidv 6351 . 2
6 df-mpt2 6301 . 2
7 df-mpt2 6301 . 2
85, 6, 73eqtr4g 2523 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  /\w3a 973  =wceq 1395  e.wcel 1818  {coprab 6297  e.cmpt2 6298
This theorem is referenced by:  mpt2eq3ia  6362  mpt2eq3dv  6363  ofeq  6542  fmpt2co  6883  mapxpen  7703  cantnffval  8101  cantnfres  8117  cantnfvalOLD  8138  sadfval  14102  smufval  14127  vdwapfval  14489  comfeq  15101  monpropd  15132  cofuval2  15256  cofuass  15258  cofulid  15259  cofurid  15260  catcisolem  15433  prfval  15468  prf1st  15473  prf2nd  15474  1st2ndprf  15475  xpcpropd  15477  curf1  15494  curfuncf  15507  curf2ndf  15516  grpsubpropd2  16141  mulgpropd  16175  oppglsm  16662  subglsm  16691  lsmpropd  16695  gsumcom2  17003  gsumdixpOLD  17257  gsumdixp  17258  psrvscafval  18043  evlslem4OLD  18173  evlslem4  18174  evlslem2  18180  psrplusgpropd  18277  mamures  18892  mpt2matmul  18948  mamutpos  18960  dmatmul  18999  dmatcrng  19004  scmatscmiddistr  19010  scmatcrng  19023  1marepvmarrepid  19077  1marepvsma1  19085  mdetrsca2  19106  mdetrlin2  19109  mdetunilem5  19118  mdetunilem6  19119  mdetunilem7  19120  mdetunilem8  19121  mdetunilem9  19122  maduval  19140  maducoeval  19141  maducoeval2  19142  madugsum  19145  madurid  19146  smadiadetglem2  19174  cramerimplem2  19186  mat2pmatghm  19231  mat2pmatmul  19232  m2cpminvid  19254  m2cpminvid2  19256  decpmatid  19271  decpmatmulsumfsupp  19274  monmatcollpw  19280  pmatcollpwscmatlem2  19291  mp2pm2mplem3  19309  mp2pm2mplem4  19310  pm2mpghm  19317  pm2mpmhmlem1  19319  ptval2  20102  cnmpt2t  20174  cnmpt22  20175  cnmptcom  20179  cnmptk2  20187  cnmpt2plusg  20587  istgp2  20590  prdstmdd  20622  cnmpt2vsca  20697  cnmpt2ds  21348  cnmpt2pc  21428  cnmpt2ip  21688  rrxds  21825  rrxmfval  21833  nvmfval  25539  pstmval  27874  sseqval  28327  cvmlift2lem6  28753  cvmlift2lem7  28754  cvmlift2lem12  28759  funcrngcsetcALT  32807  dvhfvadd  36818
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-3an 975  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