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

Theorem mpteq2dva 4297
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 1630 . 2  |-  F/ x ph
2 mpteq2dva.1 . 2  |-  ( (
ph  /\  x  e.  A )  ->  B  =  C )
31, 2mpteq2da 4296 1  |-  ( ph  ->  ( x  e.  A  |->  B )  =  ( x  e.  A  |->  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    = wceq 1653    e. wcel 1726    e. cmpt 4268
This theorem is referenced by:  mpteq2dv  4298  offval  6314  offval2  6324  caofinvl  6333  caofcom  6338  caofass  6340  caofdi  6342  caofdir  6343  caonncan  6344  curry1  6440  curry2  6443  pw2f1olem  7214  mapxpen  7275  xpmapenlem  7276  cantnfp1  7639  cantnflem1d  7646  cantnflem1  7647  cnfcom2lem  7660  dfac12lem1  8025  seqof  11382  seqof2  11383  swrd0val  11770  revco  11805  ccatco  11806  lo1eq  12364  rlimeq  12365  lo1mul2  12424  o1dif  12425  lo1sub  12426  rlimdiv  12441  caucvgr  12471  fsumrlim  12592  fsumo1  12593  climfsum  12601  geomulcvg  12655  vdwlem8  13358  restid2  13660  pwsplusgval  13714  pwsmulrval  13715  pwsvscafval  13718  divsin  13771  xpsaddlem  13802  xpsvsca  13806  catidd  13907  fuclid  14165  fucrid  14166  fucass  14167  setcepi  14245  prf1st  14303  prf2nd  14304  1st2ndprf  14305  curfcl  14331  curfuncf  14337  diag2  14344  curf2ndf  14346  hof2val  14355  hofcllem  14357  hofcl  14358  yonedalem4a  14374  yonedalem4c  14376  yonedalem3b  14378  yonedainv  14380  yonffthlem  14381  prdsidlem  14729  prdsmndd  14730  pwsco2mhm  14772  frmdup3  14813  grpinvpropd  14868  prdsinvlem  14928  pwsinvg  14932  pwssub  14933  galactghm  15108  cayleylem1  15112  sylow1lem2  15235  sylow3lem1  15263  efginvrel1  15362  frgpup3lem  15411  frgpup3  15412  prdscmnd  15478  iscyggen  15492  gsumval3  15516  gsumcllem  15518  gsumzsplit  15531  gsumsub  15544  gsum2d  15548  gsum2d2  15550  gsumxp  15552  prdsgsum  15554  dprdfsub  15581  dprdfeq0  15582  dprddisj2  15599  dprd2d2  15604  dpjidcl  15618  ablfaclem2  15646  ablfac2  15649  gsumdixp  15717  prdsmgp  15718  prdsrngd  15720  prdslmodd  16047  asclpropd  16406  psrass1lem  16444  psrlinv  16463  psrass1  16471  psrdi  16472  psrdir  16473  psrcom  16474  psrass23  16475  resspsrmul  16482  mplsubrglem  16504  mplmonmul  16529  mplcoe1  16530  mplcoe2  16532  mplcoe4  16565  psrplusgpropd  16631  psropprmul  16634  coe1mul2  16664  coe1tm  16667  coe1tmmul2  16670  coe1tmmul  16671  coe1pwmul  16673  ply1coe  16686  mulgrhm2  16790  frgpcyg  16856  phlpropd  16888  neiptopnei  17198  neiptopreu  17199  ptcnplem  17655  cnmpt1t  17699  cnmpt12  17701  cnmptkp  17714  cnmptk1  17715  cnmpt1k  17716  cnmptkk  17717  cnmptk1p  17719  cnmpt2k  17722  qtopeu  17750  pt1hmeo  17840  ptunhmeo  17842  xkocnv  17848  xkohmeo  17849  flfcnp2  18041  cnmpt1plusg  18119  istgp2  18123  tmdmulg  18124  tgpmulg  18125  tmdgsum  18127  symgtgp  18133  subgtgp  18137  tgpconcomp  18144  prdstgpd  18156  tsmsmhm  18177  tsmsadd  18178  tsmssub  18180  tgptsmscls  18181  tsmssplit  18183  tsmsxplem1  18184  tsmsxplem2  18185  cnmpt1vsca  18225  tlmtgp  18227  ustuqtoplem  18271  utopsnneip  18280  ressprdsds  18403  metuvalOLD  18581  metuval  18582  nmfval2  18640  tngnm  18694  nmoeq0  18772  idnghm  18779  cnmpt1ds  18875  fsumcn  18902  expcn  18904  divccn  18905  divccncf  18938  negcncf  18950  copco  19045  pcopt  19049  pcopt2  19050  pcoass  19051  pi1xfrcnvlem  19083  cnmpt1ip  19203  minveclem3b  19331  ovolctb  19388  ovoliunnul  19405  voliunlem3  19448  ovolfs2  19465  uniioombllem2  19477  vitalilem4  19505  vitalilem5  19506  ismbf  19524  mbfss  19540  mbfmulc2re  19542  mbfneg  19544  mbfpos  19545  mbfposb  19547  mbfadd  19555  mbfsub  19556  mbfmulc2  19557  mbfinf  19559  mbflimsup  19560  mbflimlem  19561  i1fpos  19600  i1fposd  19601  itg1climres  19608  mbfmul  19620  itg2mulc  19641  itg2i1fseq  19649  itg2cnlem1  19655  itg2cnlem2  19656  itgresr  19672  iblneg  19696  i1fibl  19701  itgitg1  19702  iblsub  19715  itgfsum  19720  itgmulc2lem1  19725  limcmpt  19772  limccnp  19780  limcco  19782  dvreslem  19798  dvres2lem  19799  dvidlem  19804  dvcnp2  19808  dvaddbr  19826  dvmulbr  19827  dvmulf  19831  dvcmulf  19833  dvcobr  19834  dvcof  19836  dvcjbr  19837  dvcj  19838  dvfre  19839  dvexp  19841  dvexp2  19842  dvrec  19843  dvmptcmul  19852  dvmptdivc  19853  dvmptneg  19854  dvmptsub  19855  dvmptre  19857  dvmptim  19858  dvmptfsum  19861  dvcnvlem  19862  dvcnv  19863  dvexp3  19864  dvef  19866  dvsincos  19867  dv11cn  19887  lhop2  19901  lhop  19902  ftc2  19930  itgparts  19933  itgsubstlem  19934  evlslem3  19937  evlslem1  19938  mdegfval  19987  mdegmullem  20003  ply1termlem  20124  plypow  20126  plyconst  20127  plyeq0lem  20131  plypf1  20133  plyaddlem1  20134  plymullem1  20135  coeeulem  20145  coeidlem  20158  plyco  20162  coeeq2  20163  0dgr  20166  0dgrb  20167  dgrcolem1  20193  dgrcolem2  20194  plycjlem  20196  dvply1  20203  dvply2g  20204  plydiveu  20217  plyremlem  20223  elqaalem3  20240  taylfval  20277  dvtaylp  20288  taylthlem1  20291  taylthlem2  20292  ulmshft  20308  mtestbdd  20323  iblulm  20325  itgulm2  20327  pserulm  20340  psercn2  20341  pserdvlem2  20346  pserdv  20347  pserdv2  20348  abelthlem1  20349  abelthlem3  20351  advlog  20547  advlogexp  20548  dvcxp1  20628  dvcxp2  20629  sqrcn  20636  loglesqr  20644  dvatan  20777  atantayl2  20780  atantayl3  20781  leibpi  20784  rlimcnp2  20807  efrlim  20810  dfef2  20811  cxp2lim  20817  divsqrsumlem  20820  ftalem7  20863  basellem9  20873  muinv  20980  logfacrlim  21010  logexprlim  21011  dchrmulid2  21038  dchrinvcl  21039  lgseisenlem3  21137  lgseisenlem4  21138  chtppilimlem2  21170  chebbnd2  21173  chpchtlim  21175  chpo1ub  21176  rpvmasumlem  21183  dchrmusumlema  21189  dchrvmasumlem1  21191  dchrvmasumiflem2  21198  dchrisum0fno1  21207  rpvmasum2  21208  dchrisum0lema  21210  dchrisum0lem1  21212  dchrisum0lem2a  21213  dchrisum0lem2  21214  dchrisum0  21216  dchrmusumlem  21218  dchrvmasumlem  21219  rpvmasum  21222  rplogsum  21223  logdivsum  21229  mulog2sumlem3  21232  vmalogdivsum2  21234  vmalogdivsum  21235  2vmadivsumlem  21236  logsqvma2  21239  log2sumbnd  21240  selberglem2  21242  selberg3lem1  21253  selberg3  21255  selberg4lem1  21256  selberg4  21257  pntrsumo1  21261  selberg3r  21265  selberg4r  21266  selberg34r  21267  pntrlog2bndlem2  21274  pntrlog2bndlem4  21276  pntrlog2bndlem5  21277  pntrlog2bndlem6  21279  padicabvf  21327  padicabvcxp  21328  chscllem4  23144  brafnmul  23456  kbmul  23460  ofresid  24057  fmptapd  24063  ofoprabco  24081  gsumsn2  24221  xrge0mulc1cn  24329  esumval  24443  esumsn  24458  esumpcvgval  24470  esumcvg  24478  ofcfeqd2  24486  meascnbl  24575  sitgval  24649  probmeasb  24690  cndprobprob  24698  dstfrvclim1  24737  ballotlemfval  24749  ballotlemsval  24768  ballotlemieq  24776  lgamgulmlem2  24816  lgamgulm2  24822  lgamcvglem  24826  gamcvg2lem  24845  ptpcon  24922  cvmliftlem6  24979  cvmliftphtlem  25006  cvmlift3lem5  25012  divcnvlin  25214  ovoliunnfl  26250  voliunnfl  26252  volsupnfl  26253  mbfposadd  26256  itg2addnclem  26258  itg2addnclem3  26260  itg2addnc  26261  itgaddnclem2  26266  itgaddnc  26267  iblsubnc  26268  itgsubnc  26269  itgmulc2nclem1  26273  itgmulc2nclem2  26274  itgmulc2nc  26275  itgabsnc  26276  ftc1cnnclem  26280  ftc1anclem3  26284  ftc1anclem5  26286  ftc1anclem6  26287  ftc1anclem8  26289  ftc1anc  26290  ftc2nc  26291  areacirclem1  26294  areacirclem2  26295  areacirclem4  26297  areacirc  26299  upixp  26433  mzpsubst  26807  mzprename  26808  mzpcompact2lem  26810  eldioph2  26822  rabdiophlem2  26864  uvcresum  27221  frlmup1  27229  grpvrinv  27430  mhmvlin  27431  mamuass  27439  mamudi  27440  mamudir  27441  mamuvs1  27442  mamuvs2  27443  mendlmod  27480  mendassa  27481  expgrowthi  27529  expgrowth  27531  mulc1cncfg  27699  expcnfg  27704  clim1fr1  27705  ibliccsinexp  27723  itgsinexplem1  27726  itgsinexp  27727  stoweidlem4  27731  stirlinglem5  27805  swrdswrd  28221  wwlknprop  28356
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-ral 2712  df-opab 4269  df-mpt 4270
  Copyright terms: Public domain W3C validator