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

Theorem mpteq2dva 4938
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 2005 . 2 𝑥𝜑
2 mpteq2dva.1 . 2 ((𝜑𝑥𝐴) → 𝐵 = 𝐶)
31, 2mpteq2da 4937 1 (𝜑 → (𝑥𝐴𝐵) = (𝑥𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1637  wcel 2156  cmpt 4923
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-ral 3101  df-opab 4907  df-mpt 4924
This theorem is referenced by:  mpteq2dv  4939  2fvcoidd  6772  offval  7130  offval2  7140  caofinvl  7150  caofcom  7155  caofass  7157  caofdi  7159  caofdir  7160  caonncan  7161  curry1  7499  curry2  7502  mpt2curryd  7626  pw2f1olem  8299  mapxpen  8361  xpmapenlem  8362  cantnfp1  8821  cantnflem1d  8828  cantnflem1  8829  cnfcom2lem  8841  dfac12lem1  9246  seqof  13077  seqof2  13078  swrd0val  13640  swrdswrd  13680  repswswrd  13751  repswrevw  13753  revco  13800  ccatco  13801  repsco  13805  ofccat  13929  lo1eq  14518  rlimeq  14519  lo1mul2  14578  o1dif  14579  lo1sub  14580  rlimdiv  14595  caucvgr  14625  sumeq1  14638  fsumrlim  14761  fsumo1  14762  climfsum  14770  geomulcvg  14825  vdwlem8  15905  prmgapprmo  15979  restid2  16292  pwsplusgval  16351  pwsmulrval  16352  pwsvscafval  16355  qusin  16405  xpsaddlem  16436  xpsvsca  16440  catidd  16541  fuclid  16826  fucrid  16827  fucass  16828  setcepi  16938  prf1st  17045  prf2nd  17046  1st2ndprf  17047  curfcl  17073  curfuncf  17079  diag2  17086  curf2ndf  17088  hof2val  17097  hofcllem  17099  hofcl  17100  yonedalem4a  17116  yonedalem4c  17118  yonedalem3b  17120  yonedainv  17122  yonffthlem  17123  prdsidlem  17523  prdsmndd  17524  pwsco2mhm  17572  frmdup3lem  17604  frmdup3  17605  grpinvpropd  17691  prdsinvlem  17725  pwsinvg  17729  pwssub  17730  galactghm  18020  cayleylem1  18029  pmtrprfval  18104  sylow1lem2  18211  sylow3lem1  18239  efginvrel1  18338  frgpup3lem  18387  frgpup3  18388  prdscmnd  18461  iscyggen  18479  gsumval3  18505  gsumcllem  18506  gsumzsplit  18524  gsumsub  18545  gsummptf1o  18559  gsum2d  18568  gsum2d2  18570  gsumxp  18572  prdsgsum  18574  telgsumfz  18585  telgsumfz0  18587  telgsum  18589  dprdfsub  18618  dprdfeq0  18619  dprddisj2  18636  dprd2d2  18641  dpjidcl  18655  ablfaclem2  18683  ablfac2  18686  srgbinomlem3  18740  srgbinomlem4  18741  srgbinomlem  18742  gsumdixp  18807  prdsmgp  18808  prdsringd  18810  prdslmodd  19172  asclpropd  19551  psrass1lem  19582  psrlinv  19602  psrass1  19610  psrdi  19611  psrdir  19612  psrass23l  19613  psrcom  19614  psrass23  19615  resspsrmul  19622  mplsubrglem  19644  mplmonmul  19669  mplcoe1  19670  mplcoe5  19673  mplcoe4  19707  evlslem3  19718  evlslem1  19719  psrplusgpropd  19810  psropprmul  19812  coe1mul2  19843  coe1tm  19847  coe1tmmul2  19850  coe1tmmul  19851  coe1pwmul  19853  cply1mul  19868  ply1coe  19870  eqcoe1ply1eq  19871  lply1binomsc  19881  evl1gsummon  19933  mulgrhm2  20051  frgpcyg  20125  evpmodpmf1o  20146  phlpropd  20206  frlmphl  20326  uvcresum  20338  frlmup1  20343  mamures  20402  grpvrinv  20408  mhmvlin  20409  mamuass  20414  mamudi  20415  mamudir  20416  mamuvs1  20417  mamuvs2  20418  mpt2matmul  20459  mamutpos  20471  madetsumid  20474  dmatmul  20510  scmatscm  20526  1mavmul  20561  mavmulass  20562  mvmumamul1  20567  mulmarep1gsum1  20586  mulmarep1gsum2  20587  mdetleib2  20601  mdetfval1  20603  mdet0pr  20605  mdetdiag  20612  mdetdiagid  20613  mdetrlin  20615  mdetrsca  20616  mdetralt  20621  mdetunilem9  20633  gsummatr01  20673  smadiadetlem1a  20677  smadiadetlem3  20682  smadiadetlem4  20683  cpmatmcllem  20732  mat2pmatmul  20745  decpmatmullem  20785  decpmatmul  20786  pmatcollpw1lem2  20789  pmatcollpw  20795  pmatcollpw3lem  20797  pmatcollpwscmat  20805  idpm2idmp  20815  mp2pm2mplem3  20822  mp2pm2mplem4  20823  mp2pm2mplem5  20824  mp2pm2mp  20825  pm2mpghm  20830  pm2mpmhmlem2  20833  monmat2matmon  20838  pm2mp  20839  chpdmat  20855  chpscmat  20856  chpscmatgsumbin  20858  chpscmatgsummon  20859  chp0mat  20860  chpidmat  20861  chfacfscmulgsum  20874  chfacfpmmulgsum  20878  chfacfpmmulgsum2  20879  cayhamlem1  20880  cpmidgsumm2pm  20883  cpmidpmat  20887  cpmadugsumlemB  20888  cpmadugsumlemC  20889  cpmadugsumlemF  20890  cpmadumatpoly  20897  cayhamlem3  20901  cayhamlem4  20902  cayleyhamilton0  20903  cayleyhamiltonALT  20905  neiptopnei  21146  neiptopreu  21147  ptcnplem  21634  cnmpt1t  21678  cnmpt12  21680  cnmptkp  21693  cnmptk1  21694  cnmpt1k  21695  cnmptkk  21696  cnmptk1p  21698  cnmpt2k  21701  qtopeu  21729  pt1hmeo  21819  ptunhmeo  21821  xkocnv  21827  xkohmeo  21828  flfcnp2  22020  cnmpt1plusg  22100  istgp2  22104  tmdmulg  22105  tgpmulg  22106  tmdgsum  22108  symgtgp  22114  subgtgp  22118  tgpconncomp  22125  prdstgpd  22137  tsmsmhm  22158  tsmsadd  22159  tsmssub  22161  tgptsmscls  22162  tsmssplit  22164  tsmsxplem1  22165  tsmsxplem2  22166  cnmpt1vsca  22206  tlmtgp  22208  ustuqtoplem  22252  utopsnneip  22261  ressprdsds  22385  metuval  22563  nmfval2  22604  tngnm  22664  nmoeq0  22749  idnghm  22756  cnmpt1ds  22854  fsumcn  22882  expcn  22884  divccn  22885  divccncf  22918  negcncf  22930  copco  23026  pcopt  23030  pcopt2  23031  pcoass  23032  pi1xfrcnvlem  23064  cnmpt1ip  23254  rrxnm  23387  rrxds  23389  minveclem3b  23407  divcncf  23424  ovolctb  23467  ovoliunnul  23484  voliunlem3  23529  ovolfs2  23548  uniioombllem2  23560  vitalilem4  23588  vitalilem5  23589  ismbf  23605  mbfss  23623  mbfmulc2re  23625  mbfneg  23627  mbfpos  23628  mbfposb  23630  mbfadd  23638  mbfsub  23639  mbfmulc2  23640  mbfinf  23642  mbflimsup  23643  mbflimlem  23644  i1fpos  23683  i1fposd  23684  itg1climres  23691  mbfmul  23703  itg2mulc  23724  itg2i1fseq  23732  itg2cnlem1  23738  itg2cnlem2  23739  itgresr  23755  iblneg  23779  i1fibl  23784  itgitg1  23785  iblsub  23798  itgfsum  23803  itgmulc2lem1  23808  limcmpt  23857  limccnp  23865  limcco  23867  dvreslem  23883  dvres2lem  23884  dvidlem  23889  dvcnp2  23893  dvaddbr  23911  dvmulbr  23912  dvmulf  23916  dvcmulf  23918  dvcobr  23919  dvcof  23921  dvcjbr  23922  dvcj  23923  dvfre  23924  dvexp  23926  dvexp2  23927  dvrec  23928  dvmptcmul  23937  dvmptdivc  23938  dvmptneg  23939  dvmptsub  23940  dvmptre  23942  dvmptim  23943  dvrecg  23946  dvmptdiv  23947  dvmptfsum  23948  dvcnvlem  23949  dvcnv  23950  dvexp3  23951  dvef  23953  dvsincos  23954  dv11cn  23974  lhop2  23988  lhop  23989  ftc2  24017  itgparts  24020  itgsubstlem  24021  mdegfval  24032  mdegmullem  24048  ply1termlem  24169  plypow  24171  plyconst  24172  plyeq0lem  24176  plypf1  24178  plyaddlem1  24179  plymullem1  24180  coeeulem  24190  coeidlem  24203  plyco  24207  coeeq2  24208  0dgr  24211  0dgrb  24212  dgrcolem1  24239  dgrcolem2  24240  plycjlem  24242  dvply1  24249  dvply2g  24250  plydiveu  24263  plyremlem  24269  elqaalem3  24286  taylfval  24323  dvtaylp  24334  taylthlem1  24337  taylthlem2  24338  ulmshft  24354  mtestbdd  24369  iblulm  24371  itgulm2  24373  pserulm  24386  psercn2  24387  pserdvlem2  24392  pserdv  24393  pserdv2  24394  abelthlem1  24395  abelthlem3  24397  advlog  24610  advlogexp  24611  dvcxp1  24691  dvcxp2  24692  dvcncxp1  24694  sqrtcn  24701  loglesqrt  24709  dvatan  24872  atantayl2  24875  atantayl3  24876  leibpi  24879  rlimcnp2  24903  efrlim  24906  dfef2  24907  cxp2lim  24913  divsqrtsumlem  24916  lgamgulmlem2  24966  lgamgulm2  24972  lgamcvglem  24976  gamcvg2lem  24995  ftalem7  25015  basellem9  25025  muinv  25129  logfacrlim  25159  logexprlim  25160  dchrmulid2  25187  dchrinvcl  25188  lgseisenlem3  25312  lgseisenlem4  25313  chtppilimlem2  25373  chebbnd2  25376  chpchtlim  25378  chpo1ub  25379  rpvmasumlem  25386  dchrmusumlema  25392  dchrvmasumlem1  25394  dchrvmasumiflem2  25401  dchrisum0fno1  25410  rpvmasum2  25411  dchrisum0lema  25413  dchrisum0lem1  25415  dchrisum0lem2a  25416  dchrisum0lem2  25417  dchrisum0  25419  dchrmusumlem  25421  dchrvmasumlem  25422  rpvmasum  25425  rplogsum  25426  logdivsum  25432  mulog2sumlem3  25435  vmalogdivsum2  25437  vmalogdivsum  25438  2vmadivsumlem  25439  logsqvma2  25442  log2sumbnd  25443  selberglem2  25445  selberg3lem1  25456  selberg3  25458  selberg4lem1  25459  selberg4  25460  pntrsumo1  25464  selberg3r  25468  selberg4r  25469  selberg34r  25470  pntrlog2bndlem2  25477  pntrlog2bndlem4  25479  pntrlog2bndlem5  25480  pntrlog2bndlem6  25482  padicabvf  25530  padicabvcxp  25531  mirval  25760  crctcshlem4  26937  clwlknf1oclwwlkn  27244  eucrct2eupth  27414  chscllem4  28823  brafnmul  29134  kbmul  29138  ofresid  29767  ofoprabco  29787  fcobijfs  29824  gsummpt2d  30102  gsummptres  30105  fzto1st1  30173  fzto1st  30174  mdetpmtr1  30210  mdetlap  30219  xrge0mulc1cn  30308  esumval  30429  esumsnf  30447  esumpcvgval  30461  esumcvg  30469  esumcvgsum  30471  esumsup  30472  ofcfeqd2  30484  meascnbl  30603  sitgval  30715  probmeasb  30813  cndprobprob  30821  dstfrvclim1  30860  ballotlemfval  30872  ballotlemsval  30891  ballotlemieq  30899  plymul02  30944  plymulx0  30945  plymulx  30946  signsplypnf  30948  signstfv  30961  signstfvn  30967  signstfvp  30969  itgexpif  31005  logdivsqrle  31049  ptpconn  31533  cvmliftlem6  31590  cvmliftphtlem  31617  cvmlift3lem5  31623  elmrsubrn  31735  msubfval  31739  msubco  31746  divcnvlin  31935  knoppcnlem9  32803  knoppcnlem10  32804  knoppcnlem11  32805  bj-finsumval0  33459  curf  33695  matunitlindflem1  33713  matunitlindflem2  33714  poimirlem3  33720  poimirlem15  33732  poimirlem16  33733  poimirlem17  33734  poimirlem19  33736  poimirlem20  33737  broucube  33751  ovoliunnfl  33759  voliunnfl  33761  volsupnfl  33762  mbfposadd  33764  itg2addnclem  33768  itg2addnclem3  33770  itg2addnc  33771  itgaddnclem2  33776  itgaddnc  33777  iblsubnc  33778  itgsubnc  33779  itgmulc2nclem1  33783  itgmulc2nclem2  33784  itgmulc2nc  33785  itgabsnc  33786  ftc1cnnclem  33790  ftc1anclem3  33794  ftc1anclem5  33796  ftc1anclem6  33797  ftc1anclem8  33799  ftc1anc  33800  ftc2nc  33801  areacirclem1  33807  areacirclem2  33808  areacirclem4  33810  areacirc  33812  upixp  33831  mzpsubst  37807  mzprename  37808  mzpcompact2lem  37810  eldioph2  37821  rabdiophlem2  37862  mendlmod  38258  mendassa  38259  areaquad  38296  fsovcnvlem  38801  hashnzfzclim  39015  expgrowthi  39026  expgrowth  39028  uzmptshftfval  39039  dvradcnv2  39040  binomcxplemrat  39043  binomcxplemfrat  39044  binomcxplemradcnv  39045  binomcxplemdvbinom  39046  binomcxplemcvg  39047  binomcxplemdvsum  39048  binomcxplemnotnn0  39049  mulc1cncfg  40295  expcnfg  40297  fprodcnlem  40305  clim1fr1  40307  divcnvg  40333  sublimc  40358  reclimc  40359  divlimc  40362  limsupresico  40406  limsuppnfdlem  40407  limsupvaluz  40414  supcnvlimsupmpt  40447  liminfresico  40477  climliminflimsupd  40507  cncfmptssg  40557  negcncfg  40568  cncficcgt0  40575  fprodcncf  40588  fprodsubrecnncnvlem  40595  fprodaddrecnncnvlem  40597  dvsinax  40601  dvasinbx  40609  dvdivf  40611  ioodvbdlimc1lem2  40621  ioodvbdlimc2lem  40623  dvnmptdivc  40627  dvxpaek  40629  dvnxpaek  40631  dvnmul  40632  dvnprodlem2  40636  ibliccsinexp  40640  itgsinexplem1  40643  itgsinexp  40644  iblempty  40654  itgcoscmulx  40658  itgsincmulx  40663  itgioocnicc  40666  iblcncfioo  40667  itgsbtaddcnst  40671  volioofmpt  40684  volicofmpt  40687  stoweidlem4  40694  stirlinglem5  40768  dirkerval  40781  dirkertrigeq  40791  dirkeritg  40792  dirkercncflem2  40794  dirkercncflem4  40796  fourierdlem16  40813  fourierdlem18  40815  fourierdlem21  40818  fourierdlem22  40819  fourierdlem28  40825  fourierdlem39  40836  fourierdlem40  40837  fourierdlem41  40838  fourierdlem53  40849  fourierdlem56  40852  fourierdlem57  40853  fourierdlem60  40856  fourierdlem61  40857  fourierdlem68  40864  fourierdlem73  40869  fourierdlem74  40870  fourierdlem75  40871  fourierdlem76  40872  fourierdlem78  40874  fourierdlem81  40877  fourierdlem82  40878  fourierdlem83  40879  fourierdlem84  40880  fourierdlem85  40881  fourierdlem88  40884  fourierdlem90  40886  fourierdlem92  40888  fourierdlem93  40889  fourierdlem95  40891  fourierdlem97  40893  fourierdlem101  40897  fourierdlem103  40899  fourierdlem104  40900  fourierdlem111  40907  fourierdlem112  40908  sqwvfoura  40918  sqwvfourb  40919  fouriersw  40921  elaa2lem  40923  etransclem4  40928  etransclem17  40941  etransclem18  40942  etransclem32  40956  etransclem46  40970  sge0z  41065  sge0revalmpt  41068  sge0tsms  41070  sge0sup  41081  sge0iunmptlemre  41105  sge0iun  41109  sge0xaddlem2  41124  ismeannd  41157  psmeasurelem  41160  meaiuninclem  41170  meaiininclem  41176  caratheodory  41218  isomenndlem  41220  ovnval  41231  hoicvrrex  41246  ovnlecvr  41248  ovncvrrp  41254  ovn0lem  41255  ovnsubaddlem1  41260  hoidmv1lelem2  41282  hoidmv1le  41284  hoidmvlelem3  41287  ovnhoilem2  41292  ovnhoi  41293  ovnlecvr2  41300  ovncvr2  41301  hspmbllem2  41317  ovolval2lem  41333  ovolval3  41337  ovolval5lem1  41342  ovolval5lem2  41343  ovnovollem1  41346  ovnovollem2  41347  vonioolem1  41370  vonicclem1  41373  vonct  41383  smflim  41461  smfinflem  41499  smflimsuplem5  41506  smfliminflem  41512  fdmdifeqresdif  42682  ply1mulgsumlem2  42737  lincvalsc0  42772  linc0scn0  42774  lincdifsn  42775  lincsum  42780  lincscm  42781  lindslinindimp2lem4  42812  lindslinindsimp2lem5  42813  lincresunit3lem2  42831  aacllem  43112  amgmwlem  43113
  Copyright terms: Public domain W3C validator