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

Theorem mpteq2dva 4106
Description: Slightly more general equality inference for the maps to notation. (Contributed by Scott Fenton, 25-Apr-2012.)
Hypothesis
Ref Expression
mpteq2dva.1  |-  ( (
ph  /\  x  e.  A )  ->  B  =  C )
Assertion
Ref Expression
mpteq2dva  |-  ( ph  ->  ( x  e.  A  |->  B )  =  ( x  e.  A  |->  C ) )
Distinct variable group:    ph, x
Allowed substitution hints:    A( x)    B( x)    C( x)

Proof of Theorem mpteq2dva
StepHypRef Expression
1 nfv 1605 . 2  |-  F/ x ph
2 mpteq2dva.1 . 2  |-  ( (
ph  /\  x  e.  A )  ->  B  =  C )
31, 2mpteq2da 4105 1  |-  ( ph  ->  ( x  e.  A  |->  B )  =  ( x  e.  A  |->  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1623    e. wcel 1684    e. cmpt 4077
This theorem is referenced by:  mpteq2dv  4107  offval  6085  offval2  6095  caofinvl  6104  caofcom  6109  caofass  6111  caofdi  6113  caofdir  6114  caonncan  6115  curry1  6210  curry2  6213  pw2f1olem  6966  mapxpen  7027  xpmapenlem  7028  cantnfp1  7383  cantnflem1d  7390  cantnflem1  7391  cnfcom2lem  7404  dfac12lem1  7769  seqof  11103  swrd0val  11454  revco  11489  ccatco  11490  lo1eq  12042  rlimeq  12043  lo1mul2  12102  o1dif  12103  lo1sub  12104  rlimdiv  12119  caucvgr  12148  fsumrlim  12269  fsumo1  12270  climfsum  12278  geomulcvg  12332  vdwlem8  13035  restid2  13335  pwsplusgval  13389  pwsmulrval  13390  pwsvscafval  13393  divsin  13446  xpsaddlem  13477  xpsvsca  13481  catidd  13582  cidpropd  13613  monpropd  13640  fuclid  13840  fucrid  13841  fucass  13842  setcepi  13920  prf1st  13978  prf2nd  13979  1st2ndprf  13980  curfcl  14006  curfuncf  14012  diag2  14019  curf2ndf  14021  hof2val  14030  hofcllem  14032  hofcl  14033  yonedalem4a  14049  yonedalem4c  14051  yonedalem3b  14053  yonedainv  14055  yonffthlem  14056  prdsidlem  14404  prdsmndd  14405  pwsco2mhm  14447  frmdup3  14488  grpinvpropd  14543  prdsinvlem  14603  pwsinvg  14607  pwssub  14608  galactghm  14783  cayleylem1  14787  sylow1lem2  14910  sylow3lem1  14938  efginvrel1  15037  frgpup3lem  15086  frgpup3  15087  prdscmnd  15153  iscyggen  15167  gsumval3  15191  gsumcllem  15193  gsumzsplit  15206  gsumsub  15219  gsum2d  15223  gsum2d2  15225  gsumxp  15227  prdsgsum  15229  dprdfsub  15256  dprdfeq0  15257  dprddisj2  15274  dprd2d2  15279  dpjidcl  15293  ablfaclem2  15321  ablfac2  15324  gsumdixp  15392  prdsmgp  15393  prdsrngd  15395  prdslmodd  15726  asclpropd  16085  psrass1lem  16123  psrlinv  16142  psrass1  16150  psrdi  16151  psrdir  16152  psrcom  16153  psrass23  16154  resspsrmul  16161  mplsubrglem  16183  mplmonmul  16208  mplcoe1  16209  mplcoe2  16211  mplcoe4  16244  psrplusgpropd  16313  psropprmul  16316  coe1mul2  16346  coe1tm  16349  coe1tmmul2  16352  coe1tmmul  16353  coe1pwmul  16355  ply1coe  16368  mulgrhm2  16461  frgpcyg  16527  phlpropd  16559  ptcnplem  17315  cnmpt1t  17359  cnmpt12  17361  cnmptkp  17374  cnmptk1  17375  cnmpt1k  17376  cnmptkk  17377  cnmptk1p  17379  cnmpt2k  17382  qtopeu  17407  pt1hmeo  17497  ptunhmeo  17499  xkocnv  17505  xkohmeo  17506  flfcnp2  17702  cnmpt1plusg  17770  istgp2  17774  tmdmulg  17775  tgpmulg  17776  tmdgsum  17778  symgtgp  17784  subgtgp  17788  tgpconcomp  17795  prdstgpd  17807  tsmsmhm  17828  tsmsadd  17829  tsmssub  17831  tgptsmscls  17832  tsmssplit  17834  tsmsxplem1  17835  tsmsxplem2  17836  cnmpt1vsca  17876  tlmtgp  17878  ressprdsds  17935  nmfval2  18113  tngnm  18167  nmoeq0  18245  idnghm  18252  cnmpt1ds  18347  fsumcn  18374  expcn  18376  divccn  18377  divccncf  18410  negcncf  18421  copco  18516  pcopt  18520  pcopt2  18521  pcoass  18522  pi1xfrcnvlem  18554  cnmpt1ip  18674  minveclem3b  18792  ovolctb  18849  ovoliunnul  18866  voliunlem3  18909  ovolfs2  18926  uniioombllem2  18938  vitalilem4  18966  vitalilem5  18967  ismbf  18985  mbfss  19001  mbfmulc2re  19003  mbfneg  19005  mbfpos  19006  mbfposb  19008  mbfadd  19016  mbfsub  19017  mbfmulc2  19018  mbfinf  19020  mbflimsup  19021  mbflimlem  19022  i1fpos  19061  i1fposd  19062  itg1climres  19069  mbfmul  19081  itg2mulc  19102  itg2i1fseq  19110  itg2cnlem1  19116  itg2cnlem2  19117  itgresr  19133  iblneg  19157  i1fibl  19162  itgitg1  19163  iblsub  19176  itgfsum  19181  itgmulc2lem1  19186  limcmpt  19233  limccnp  19241  limcco  19243  dvreslem  19259  dvres2lem  19260  dvidlem  19265  dvcnp2  19269  dvaddbr  19287  dvmulbr  19288  dvmulf  19292  dvcmulf  19294  dvcobr  19295  dvcof  19297  dvcjbr  19298  dvcj  19299  dvfre  19300  dvexp  19302  dvexp2  19303  dvrec  19304  dvmptcmul  19313  dvmptdivc  19314  dvmptneg  19315  dvmptsub  19316  dvmptre  19318  dvmptim  19319  dvmptfsum  19322  dvcnvlem  19323  dvcnv  19324  dvexp3  19325  dvef  19327  dvsincos  19328  dv11cn  19348  lhop2  19362  lhop  19363  ftc2  19391  itgparts  19394  itgsubstlem  19395  evlslem3  19398  evlslem1  19399  mdegfval  19448  mdegmullem  19464  ply1termlem  19585  plypow  19587  plyconst  19588  plyeq0lem  19592  plypf1  19594  plyaddlem1  19595  plymullem1  19596  coeeulem  19606  coeidlem  19619  plyco  19623  coeeq2  19624  0dgr  19627  0dgrb  19628  dgrcolem1  19654  dgrcolem2  19655  plycjlem  19657  dvply1  19664  dvply2g  19665  plydiveu  19678  plyremlem  19684  elqaalem3  19701  taylfval  19738  dvtaylp  19749  taylthlem1  19752  taylthlem2  19753  ulmshft  19769  iblulm  19783  itgulm2  19785  pserulm  19798  psercn2  19799  pserdvlem2  19804  pserdv  19805  pserdv2  19806  abelthlem1  19807  abelthlem3  19809  advlog  20001  advlogexp  20002  dvcxp1  20082  dvcxp2  20083  sqrcn  20090  loglesqr  20098  dvatan  20231  atantayl2  20234  atantayl3  20235  leibpi  20238  rlimcnp2  20261  efrlim  20264  dfef2  20265  cxp2lim  20271  divsqrsumlem  20274  ftalem7  20316  basellem9  20326  muinv  20433  logfacrlim  20463  logexprlim  20464  dchrmulid2  20491  dchrinvcl  20492  lgseisenlem3  20590  lgseisenlem4  20591  chtppilimlem2  20623  chebbnd2  20626  chpchtlim  20628  chpo1ub  20629  rpvmasumlem  20636  dchrmusumlema  20642  dchrvmasumlem1  20644  dchrvmasumiflem2  20651  dchrisum0fno1  20660  rpvmasum2  20661  dchrisum0lema  20663  dchrisum0lem1  20665  dchrisum0lem2a  20666  dchrisum0lem2  20667  dchrisum0  20669  dchrmusumlem  20671  dchrvmasumlem  20672  rpvmasum  20675  rplogsum  20676  logdivsum  20682  mulog2sumlem3  20685  vmalogdivsum2  20687  vmalogdivsum  20688  2vmadivsumlem  20689  logsqvma2  20692  log2sumbnd  20693  selberglem2  20695  selberg3lem1  20706  selberg3  20708  selberg4lem1  20709  selberg4  20710  pntrsumo1  20714  selberg3r  20718  selberg4r  20719  selberg34r  20720  pntrlog2bndlem2  20727  pntrlog2bndlem4  20729  pntrlog2bndlem5  20730  pntrlog2bndlem6  20732  padicabvf  20780  padicabvcxp  20781  chscllem4  22219  brafnmul  22531  kbmul  22535  ballotlemfval  23048  ballotlemsval  23067  ballotlemieq  23075  fmptapd  23213  ofoprabco  23232  gsumsn2  23378  esumval  23425  esumsn  23437  esumpcvgval  23446  esumcvg  23454  ofcfeqd2  23462  meascnbl  23546  probmeasb  23633  dstfrvclim1  23678  ptpcon  23764  cvmliftlem6  23821  cvmliftphtlem  23848  cvmlift3lem5  23854  areacirclem2  24925  areacirclem4  24927  areacirclem5  24929  areacirc  24931  curgrpact  25372  cmprtr  25396  cmpltr2  25407  cmperltr  25409  cmprltr  25410  addcomv  25655  addassv  25656  addidv2  25657  cnegvex2  25660  rnegvex2  25661  issubrv  25672  mulone  25685  mulmulvec  25687  distmlva  25688  distsava  25689  upixp  26403  mzpsubst  26826  mzprename  26827  mzpcompact2lem  26829  eldioph2  26841  rabdiophlem2  26883  uvcresum  27242  frlmup1  27250  grpvrinv  27451  mhmvlin  27452  mamuass  27460  mamudi  27461  mamudir  27462  mamuvs1  27463  mamuvs2  27464  mendlmod  27501  mendassa  27502  expgrowthi  27550  expgrowth  27552  mulc1cncfg  27721  expcnfg  27726  clim1fr1  27727  ibliccsinexp  27745  itgsinexplem1  27748  itgsinexp  27749  stirlinglem5  27827
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-ral 2548  df-opab 4078  df-mpt 4079
  Copyright terms: Public domain W3C validator