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

Theorem mpteq2dva 5153
Description: Slightly more general equality inference for the maps-to notation. (Contributed by Scott Fenton, 25-Apr-2012.)
Hypothesis
Ref Expression
mpteq2dva.1 ((𝜑𝑥𝐴) → 𝐵 = 𝐶)
Assertion
Ref Expression
mpteq2dva (𝜑 → (𝑥𝐴𝐵) = (𝑥𝐴𝐶))
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)   𝐶(𝑥)

Proof of Theorem mpteq2dva
StepHypRef Expression
1 nfv 1906 . 2 𝑥𝜑
2 mpteq2dva.1 . 2 ((𝜑𝑥𝐴) → 𝐵 = 𝐶)
31, 2mpteq2da 5152 1 (𝜑 → (𝑥𝐴𝐵) = (𝑥𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1528  wcel 2105  cmpt 5138
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-12 2167  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-ral 3143  df-opab 5121  df-mpt 5139
This theorem is referenced by:  mpteq2dv  5154  2fvcoidd  7044  offval  7405  offval2  7415  caofinvl  7425  caofcom  7430  caofass  7432  caofdi  7434  caofdir  7435  caonncan  7436  curry1  7790  curry2  7793  mpocurryd  7926  pw2f1olem  8610  mapxpen  8672  xpmapenlem  8673  cantnfp1  9133  cantnflem1d  9140  cantnflem1  9141  cnfcom2lem  9153  dfac12lem1  9558  seqof  13417  seqof2  13418  swrdswrd  14057  repswswrd  14136  repswrevw  14139  revco  14186  ccatco  14187  repsco  14192  ofccat  14319  lo1eq  14915  rlimeq  14916  lo1mul2  14975  o1dif  14976  lo1sub  14977  rlimdiv  14992  caucvgr  15022  sumeq1  15035  fsumrlim  15156  fsumo1  15157  climfsum  15165  geomulcvg  15222  vdwlem8  16314  prmgapprmo  16388  restid2  16694  pwsplusgval  16753  pwsmulrval  16754  pwsvscafval  16757  qusin  16807  xpsaddlem  16836  xpsvsca  16840  catidd  16941  fuclid  17226  fucrid  17227  fucass  17228  setcepi  17338  prf1st  17444  prf2nd  17445  1st2ndprf  17446  curfcl  17472  curfuncf  17478  diag2  17485  curf2ndf  17487  hof2val  17496  hofcllem  17498  hofcl  17499  yonedalem4a  17515  yonedalem4c  17517  yonedalem3b  17519  yonedainv  17521  yonffthlem  17522  prdsidlem  17933  prdsmndd  17934  pwsco2mhm  17987  frmdup3lem  18021  frmdup3  18022  grpinvpropd  18114  prdsinvlem  18148  pwsinvg  18152  pwssub  18153  galactghm  18463  cayleylem1  18471  pmtrprfval  18546  sylow1lem2  18655  sylow3lem1  18683  efginvrel1  18785  frgpup3lem  18834  frgpup3  18835  prdscmnd  18912  iscyggen  18930  gsumval3  18958  gsumcllem  18959  gsumzsplit  18978  gsumsub  18999  gsummptf1o  19014  gsum2d  19023  gsum2d2  19025  gsumxp  19027  prdsgsum  19032  telgsumfz  19041  telgsumfz0  19043  telgsum  19045  dprdfsub  19074  dprdfeq0  19075  dprddisj2  19092  dprd2d2  19097  dpjidcl  19111  ablfaclem2  19139  ablfac2  19142  srgbinomlem3  19223  srgbinomlem4  19224  srgbinomlem  19225  gsumdixp  19290  prdsmgp  19291  prdsringd  19293  prdslmodd  19672  asclpropd  20056  psrass1lem  20087  psrlinv  20107  psrass1  20115  psrdi  20116  psrdir  20117  psrass23l  20118  psrcom  20119  psrass23  20120  resspsrmul  20127  mplsubrglem  20149  mplmonmul  20175  mplcoe1  20176  mplcoe5  20179  mplcoe4  20213  evlslem3  20223  evlslem1  20225  psrplusgpropd  20334  psropprmul  20336  coe1mul2  20367  coe1tm  20371  coe1tmmul2  20374  coe1tmmul  20375  coe1pwmul  20377  cply1mul  20392  ply1coe  20394  eqcoe1ply1eq  20395  lply1binomsc  20405  evl1gsummon  20458  mulgrhm2  20576  frgpcyg  20650  evpmodpmf1o  20670  phlpropd  20729  frlmphl  20855  uvcresum  20867  frlmup1  20872  mamures  20931  grpvrinv  20937  mhmvlin  20938  mamuass  20941  mamudi  20942  mamudir  20943  mamuvs1  20944  mamuvs2  20945  mpomatmul  20985  mamutpos  20997  madetsumid  21000  dmatmul  21036  scmatscm  21052  1mavmul  21087  mavmulass  21088  mvmumamul1  21093  mulmarep1gsum1  21112  mulmarep1gsum2  21113  mdetleib2  21127  mdetfval1  21129  mdet0pr  21131  mdetdiag  21138  mdetdiagid  21139  mdetrlin  21141  mdetrsca  21142  mdetralt  21147  mdetunilem9  21159  gsummatr01  21198  smadiadetlem1a  21202  smadiadetlem3  21207  smadiadetlem4  21208  cpmatmcllem  21256  mat2pmatmul  21269  decpmatmullem  21309  decpmatmul  21310  pmatcollpw1lem2  21313  pmatcollpw  21319  pmatcollpw3lem  21321  pmatcollpwscmat  21329  idpm2idmp  21339  mp2pm2mplem3  21346  mp2pm2mplem4  21347  mp2pm2mplem5  21348  mp2pm2mp  21349  pm2mpghm  21354  pm2mpmhmlem2  21357  monmat2matmon  21362  pm2mp  21363  chpdmat  21379  chpscmat  21380  chpscmatgsumbin  21382  chpscmatgsummon  21383  chp0mat  21384  chpidmat  21385  chfacfscmulgsum  21398  chfacfpmmulgsum  21402  chfacfpmmulgsum2  21403  cayhamlem1  21404  cpmidgsumm2pm  21407  cpmidpmat  21411  cpmadugsumlemB  21412  cpmadugsumlemC  21413  cpmadugsumlemF  21414  cpmadumatpoly  21421  cayhamlem3  21425  cayhamlem4  21426  cayleyhamilton0  21427  cayleyhamiltonALT  21429  neiptopnei  21670  neiptopreu  21671  ptcnplem  22159  cnmpt1t  22203  cnmpt12  22205  cnmptkp  22218  cnmptk1  22219  cnmpt1k  22220  cnmptkk  22221  cnmptk1p  22223  cnmpt2k  22226  qtopeu  22254  pt1hmeo  22344  ptunhmeo  22346  xkocnv  22352  xkohmeo  22353  flfcnp2  22545  cnmpt1plusg  22625  istgp2  22629  tmdmulg  22630  tgpmulg  22631  tmdgsum  22633  symgtgp  22639  subgtgp  22643  tgpconncomp  22650  prdstgpd  22662  tsmsmhm  22683  tsmsadd  22684  tsmssub  22686  tgptsmscls  22687  tsmssplit  22689  tsmsxplem1  22690  tsmsxplem2  22691  cnmpt1vsca  22731  tlmtgp  22733  ustuqtoplem  22777  utopsnneip  22786  ressprdsds  22910  metuval  23088  nmfval2  23129  tngnm  23189  nmoeq0  23274  idnghm  23281  cnmpt1ds  23379  fsumcn  23407  expcn  23409  divccn  23410  divccncf  23443  negcncf  23455  copco  23551  pcopt  23555  pcopt2  23556  pcoass  23557  pi1xfrcnvlem  23589  cnmpt1ip  23779  rrxnm  23923  rrxds  23925  minveclem3b  23960  divcncf  23977  ovolctb  24020  ovoliunnul  24037  voliunlem3  24082  ovolfs2  24101  uniioombllem2  24113  vitalilem4  24141  vitalilem5  24142  ismbf  24158  mbfss  24176  mbfmulc2re  24178  mbfneg  24180  mbfpos  24181  mbfposb  24183  mbfadd  24191  mbfsub  24192  mbfmulc2  24193  mbfinf  24195  mbflimsup  24196  mbflimlem  24197  i1fpos  24236  i1fposd  24237  itg1climres  24244  mbfmul  24256  itg2mulc  24277  itg2i1fseq  24285  itg2cnlem1  24291  itg2cnlem2  24292  itgresr  24308  iblneg  24332  i1fibl  24337  itgitg1  24338  iblsub  24351  itgfsum  24356  itgmulc2lem1  24361  limcmpt  24410  limccnp  24418  limcco  24420  dvreslem  24436  dvres2lem  24437  dvidlem  24442  dvcnp2  24446  dvaddbr  24464  dvmulbr  24465  dvmulf  24469  dvcmulf  24471  dvcobr  24472  dvcof  24474  dvcjbr  24475  dvcj  24476  dvfre  24477  dvexp  24479  dvexp2  24480  dvrec  24481  dvmptcmul  24490  dvmptdivc  24491  dvmptneg  24492  dvmptsub  24493  dvmptre  24495  dvmptim  24496  dvrecg  24499  dvmptdiv  24500  dvmptfsum  24501  dvcnvlem  24502  dvcnv  24503  dvexp3  24504  dvef  24506  dvsincos  24507  dv11cn  24527  lhop2  24541  lhop  24542  ftc2  24570  itgparts  24573  itgsubstlem  24574  mdegfval  24585  mdegmullem  24601  ply1termlem  24722  plypow  24724  plyconst  24725  plyeq0lem  24729  plypf1  24731  plyaddlem1  24732  plymullem1  24733  coeeulem  24743  coeidlem  24756  plyco  24760  coeeq2  24761  0dgr  24764  0dgrb  24765  dgrcolem1  24792  dgrcolem2  24793  plycjlem  24795  dvply1  24802  dvply2g  24803  plydiveu  24816  plyremlem  24822  elqaalem3  24839  taylfval  24876  dvtaylp  24887  taylthlem1  24890  taylthlem2  24891  ulmshft  24907  mtestbdd  24922  iblulm  24924  itgulm2  24926  pserulm  24939  psercn2  24940  pserdvlem2  24945  pserdv  24946  pserdv2  24947  abelthlem1  24948  abelthlem3  24950  advlog  25164  advlogexp  25165  dvcxp1  25248  dvcxp2  25249  dvcncxp1  25251  sqrtcn  25258  loglesqrt  25266  dvatan  25440  atantayl2  25443  atantayl3  25444  leibpi  25448  rlimcnp2  25472  efrlim  25475  dfef2  25476  cxp2lim  25482  divsqrtsumlem  25485  lgamgulmlem2  25535  lgamgulm2  25541  lgamcvglem  25545  gamcvg2lem  25564  ftalem7  25584  basellem9  25594  muinv  25698  logfacrlim  25728  logexprlim  25729  dchrmulid2  25756  dchrinvcl  25757  lgseisenlem3  25881  lgseisenlem4  25882  chtppilimlem2  25978  chebbnd2  25981  chpchtlim  25983  chpo1ub  25984  rpvmasumlem  25991  dchrmusumlema  25997  dchrvmasumlem1  25999  dchrvmasumiflem2  26006  dchrisum0fno1  26015  rpvmasum2  26016  dchrisum0lema  26018  dchrisum0lem1  26020  dchrisum0lem2a  26021  dchrisum0lem2  26022  dchrisum0  26024  dchrmusumlem  26026  dchrvmasumlem  26027  rpvmasum  26030  rplogsum  26031  logdivsum  26037  mulog2sumlem3  26040  vmalogdivsum2  26042  vmalogdivsum  26043  2vmadivsumlem  26044  logsqvma2  26047  log2sumbnd  26048  selberglem2  26050  selberg3lem1  26061  selberg3  26063  selberg4lem1  26064  selberg4  26065  pntrsumo1  26069  selberg3r  26073  selberg4r  26074  selberg34r  26075  pntrlog2bndlem2  26082  pntrlog2bndlem4  26084  pntrlog2bndlem5  26085  pntrlog2bndlem6  26087  padicabvf  26135  padicabvcxp  26136  mirval  26369  crctcshlem4  27526  clwlknf1oclwwlkn  27791  eucrct2eupth  27952  chscllem4  29345  brafnmul  29656  kbmul  29660  cofmpt2  30308  ofresid  30318  ofoprabco  30338  fcobijfs  30386  gsummpt2d  30615  gsummptres  30618  fzto1st1  30672  fzto1st  30673  freshmansdream  30787  lbsdiflsp0  30922  fedgmullem1  30925  fedgmullem2  30926  mdetpmtr1  30988  mdetlap  30997  xrge0mulc1cn  31084  esumval  31205  esumsnf  31223  esumpcvgval  31237  esumcvg  31245  esumcvgsum  31247  esumsup  31248  ofcfeqd2  31260  meascnbl  31378  sitgval  31490  probmeasb  31588  cndprobprob  31596  dstfrvclim1  31635  ballotlemfval  31647  ballotlemsval  31666  ballotlemieq  31674  plymul02  31716  plymulx0  31717  plymulx  31718  signsplypnf  31720  signstfv  31733  signstfvn  31739  signstfvp  31741  itgexpif  31777  logdivsqrle  31821  ptpconn  32378  cvmliftlem6  32435  cvmliftphtlem  32462  cvmlift3lem5  32468  elmrsubrn  32665  msubfval  32669  msubco  32676  divcnvlin  32862  knoppcnlem9  33738  knoppcnlem10  33739  knoppcnlem11  33740  bj-finsumval0  34456  curf  34752  matunitlindflem1  34770  matunitlindflem2  34771  poimirlem3  34777  poimirlem15  34789  poimirlem16  34790  poimirlem17  34791  poimirlem19  34793  poimirlem20  34794  broucube  34808  ovoliunnfl  34816  voliunnfl  34818  volsupnfl  34819  mbfposadd  34821  itg2addnclem  34825  itg2addnclem3  34827  itg2addnc  34828  itgaddnclem2  34833  itgaddnc  34834  iblsubnc  34835  itgsubnc  34836  itgmulc2nclem1  34840  itgmulc2nclem2  34841  itgmulc2nc  34842  itgabsnc  34843  ftc1cnnclem  34847  ftc1anclem3  34851  ftc1anclem5  34853  ftc1anclem6  34854  ftc1anclem8  34856  ftc1anc  34857  ftc2nc  34858  areacirclem1  34864  areacirclem2  34865  areacirclem4  34867  areacirc  34869  upixp  34887  qsalrel  39005  mzpsubst  39225  mzprename  39226  mzpcompact2lem  39228  eldioph2  39239  rabdiophlem2  39279  mendlmod  39673  mendassa  39674  areaquad  39703  fsovcnvlem  40239  hashnzfzclim  40534  expgrowthi  40545  expgrowth  40547  uzmptshftfval  40558  dvradcnv2  40559  binomcxplemrat  40562  binomcxplemfrat  40563  binomcxplemradcnv  40564  binomcxplemdvbinom  40565  binomcxplemcvg  40566  binomcxplemdvsum  40567  binomcxplemnotnn0  40568  mulc1cncfg  41750  expcnfg  41752  fprodcnlem  41760  clim1fr1  41762  divcnvg  41788  sublimc  41813  reclimc  41814  divlimc  41817  limsupresico  41861  limsuppnfdlem  41862  limsupvaluz  41869  supcnvlimsupmpt  41902  liminfresico  41932  climliminflimsupd  41962  cncfmptssg  42033  negcncfg  42044  cncficcgt0  42051  fprodcncf  42064  fprodsubrecnncnvlem  42071  fprodaddrecnncnvlem  42073  dvsinax  42077  dvasinbx  42085  dvdivf  42087  ioodvbdlimc1lem2  42097  ioodvbdlimc2lem  42099  dvnmptdivc  42103  dvxpaek  42105  dvnxpaek  42107  dvnmul  42108  dvnprodlem2  42112  ibliccsinexp  42116  itgsinexplem1  42119  itgsinexp  42120  iblempty  42130  itgcoscmulx  42134  itgsincmulx  42139  itgioocnicc  42142  iblcncfioo  42143  itgsbtaddcnst  42147  volioofmpt  42160  volicofmpt  42163  stoweidlem4  42170  stirlinglem5  42244  dirkerval  42257  dirkertrigeq  42267  dirkeritg  42268  dirkercncflem2  42270  dirkercncflem4  42272  fourierdlem16  42289  fourierdlem18  42291  fourierdlem21  42294  fourierdlem22  42295  fourierdlem28  42301  fourierdlem39  42312  fourierdlem40  42313  fourierdlem41  42314  fourierdlem53  42325  fourierdlem56  42328  fourierdlem57  42329  fourierdlem60  42332  fourierdlem61  42333  fourierdlem68  42340  fourierdlem73  42345  fourierdlem74  42346  fourierdlem75  42347  fourierdlem76  42348  fourierdlem78  42350  fourierdlem81  42353  fourierdlem82  42354  fourierdlem83  42355  fourierdlem84  42356  fourierdlem85  42357  fourierdlem88  42360  fourierdlem90  42362  fourierdlem92  42364  fourierdlem93  42365  fourierdlem95  42367  fourierdlem97  42369  fourierdlem101  42373  fourierdlem103  42375  fourierdlem104  42376  fourierdlem111  42383  fourierdlem112  42384  sqwvfoura  42394  sqwvfourb  42395  fouriersw  42397  elaa2lem  42399  etransclem4  42404  etransclem17  42417  etransclem18  42418  etransclem32  42432  etransclem46  42446  sge0z  42538  sge0revalmpt  42541  sge0tsms  42543  sge0sup  42554  sge0iunmptlemre  42578  sge0iun  42582  sge0xaddlem2  42597  ismeannd  42630  psmeasurelem  42633  meaiuninclem  42643  meaiininclem  42649  caratheodory  42691  isomenndlem  42693  ovnval  42704  hoicvrrex  42719  ovnlecvr  42721  ovncvrrp  42727  ovn0lem  42728  ovnsubaddlem1  42733  hoidmv1lelem2  42755  hoidmv1le  42757  hoidmvlelem3  42760  ovnhoilem2  42765  ovnhoi  42766  ovnlecvr2  42773  ovncvr2  42774  hspmbllem2  42790  ovolval2lem  42806  ovolval3  42810  ovolval5lem1  42815  ovolval5lem2  42816  ovnovollem1  42819  ovnovollem2  42820  vonioolem1  42843  vonicclem1  42846  vonct  42856  smflim  42934  smfinflem  42972  smflimsuplem5  42979  smfliminflem  42985  smndex1gid  43973  smndex1igid  43974  fdmdifeqresdif  44288  ply1mulgsumlem2  44339  lincvalsc0  44374  linc0scn0  44376  lincdifsn  44377  lincsum  44382  lincscm  44383  lindslinindimp2lem4  44414  lindslinindsimp2lem5  44415  lincresunit3lem2  44433  aacllem  44800  amgmwlem  44801
  Copyright terms: Public domain W3C validator