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

Theorem mpteq2dva 5158
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 1908 . 2 𝑥𝜑
2 mpteq2dva.1 . 2 ((𝜑𝑥𝐴) → 𝐵 = 𝐶)
31, 2mpteq2da 5157 1 (𝜑 → (𝑥𝐴𝐵) = (𝑥𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1530  wcel 2107  cmpt 5143
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-12 2169  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-ral 3148  df-opab 5126  df-mpt 5144
This theorem is referenced by:  mpteq2dv  5159  2fvcoidd  7049  offval  7410  offval2  7420  caofinvl  7430  caofcom  7435  caofass  7437  caofdi  7439  caofdir  7440  caonncan  7441  curry1  7795  curry2  7798  mpocurryd  7931  pw2f1olem  8615  mapxpen  8677  xpmapenlem  8678  cantnfp1  9138  cantnflem1d  9145  cantnflem1  9146  cnfcom2lem  9158  dfac12lem1  9563  seqof  13422  seqof2  13423  swrdswrd  14062  repswswrd  14141  repswrevw  14144  revco  14191  ccatco  14192  repsco  14197  ofccat  14324  lo1eq  14920  rlimeq  14921  lo1mul2  14980  o1dif  14981  lo1sub  14982  rlimdiv  14997  caucvgr  15027  sumeq1  15040  fsumrlim  15161  fsumo1  15162  climfsum  15170  geomulcvg  15227  vdwlem8  16319  prmgapprmo  16393  restid2  16699  pwsplusgval  16758  pwsmulrval  16759  pwsvscafval  16762  qusin  16812  xpsaddlem  16841  xpsvsca  16845  catidd  16946  fuclid  17231  fucrid  17232  fucass  17233  setcepi  17343  prf1st  17449  prf2nd  17450  1st2ndprf  17451  curfcl  17477  curfuncf  17483  diag2  17490  curf2ndf  17492  hof2val  17501  hofcllem  17503  hofcl  17504  yonedalem4a  17520  yonedalem4c  17522  yonedalem3b  17524  yonedainv  17526  yonffthlem  17527  prdsidlem  17938  prdsmndd  17939  pwsco2mhm  17992  frmdup3lem  18026  frmdup3  18027  grpinvpropd  18119  prdsinvlem  18153  pwsinvg  18157  pwssub  18158  galactghm  18468  cayleylem1  18476  pmtrprfval  18551  sylow1lem2  18660  sylow3lem1  18688  efginvrel1  18790  frgpup3lem  18839  frgpup3  18840  prdscmnd  18917  iscyggen  18935  gsumval3  18963  gsumcllem  18964  gsumzsplit  18983  gsumsub  19004  gsummptf1o  19019  gsum2d  19028  gsum2d2  19030  gsumxp  19032  prdsgsum  19037  telgsumfz  19046  telgsumfz0  19048  telgsum  19050  dprdfsub  19079  dprdfeq0  19080  dprddisj2  19097  dprd2d2  19102  dpjidcl  19116  ablfaclem2  19144  ablfac2  19147  srgbinomlem3  19228  srgbinomlem4  19229  srgbinomlem  19230  gsumdixp  19295  prdsmgp  19296  prdsringd  19298  prdslmodd  19677  asclpropd  20061  psrass1lem  20092  psrlinv  20112  psrass1  20120  psrdi  20121  psrdir  20122  psrass23l  20123  psrcom  20124  psrass23  20125  resspsrmul  20132  mplsubrglem  20154  mplmonmul  20180  mplcoe1  20181  mplcoe5  20184  mplcoe4  20218  evlslem3  20228  evlslem1  20230  psrplusgpropd  20339  psropprmul  20341  coe1mul2  20372  coe1tm  20376  coe1tmmul2  20379  coe1tmmul  20380  coe1pwmul  20382  cply1mul  20397  ply1coe  20399  eqcoe1ply1eq  20400  lply1binomsc  20410  evl1gsummon  20463  mulgrhm2  20581  frgpcyg  20655  evpmodpmf1o  20675  phlpropd  20734  frlmphl  20860  uvcresum  20872  frlmup1  20877  mamures  20936  grpvrinv  20942  mhmvlin  20943  mamuass  20946  mamudi  20947  mamudir  20948  mamuvs1  20949  mamuvs2  20950  mpomatmul  20990  mamutpos  21002  madetsumid  21005  dmatmul  21041  scmatscm  21057  1mavmul  21092  mavmulass  21093  mvmumamul1  21098  mulmarep1gsum1  21117  mulmarep1gsum2  21118  mdetleib2  21132  mdetfval1  21134  mdet0pr  21136  mdetdiag  21143  mdetdiagid  21144  mdetrlin  21146  mdetrsca  21147  mdetralt  21152  mdetunilem9  21164  gsummatr01  21203  smadiadetlem1a  21207  smadiadetlem3  21212  smadiadetlem4  21213  cpmatmcllem  21261  mat2pmatmul  21274  decpmatmullem  21314  decpmatmul  21315  pmatcollpw1lem2  21318  pmatcollpw  21324  pmatcollpw3lem  21326  pmatcollpwscmat  21334  idpm2idmp  21344  mp2pm2mplem3  21351  mp2pm2mplem4  21352  mp2pm2mplem5  21353  mp2pm2mp  21354  pm2mpghm  21359  pm2mpmhmlem2  21362  monmat2matmon  21367  pm2mp  21368  chpdmat  21384  chpscmat  21385  chpscmatgsumbin  21387  chpscmatgsummon  21388  chp0mat  21389  chpidmat  21390  chfacfscmulgsum  21403  chfacfpmmulgsum  21407  chfacfpmmulgsum2  21408  cayhamlem1  21409  cpmidgsumm2pm  21412  cpmidpmat  21416  cpmadugsumlemB  21417  cpmadugsumlemC  21418  cpmadugsumlemF  21419  cpmadumatpoly  21426  cayhamlem3  21430  cayhamlem4  21431  cayleyhamilton0  21432  cayleyhamiltonALT  21434  neiptopnei  21675  neiptopreu  21676  ptcnplem  22164  cnmpt1t  22208  cnmpt12  22210  cnmptkp  22223  cnmptk1  22224  cnmpt1k  22225  cnmptkk  22226  cnmptk1p  22228  cnmpt2k  22231  qtopeu  22259  pt1hmeo  22349  ptunhmeo  22351  xkocnv  22357  xkohmeo  22358  flfcnp2  22550  cnmpt1plusg  22630  istgp2  22634  tmdmulg  22635  tgpmulg  22636  tmdgsum  22638  symgtgp  22644  subgtgp  22648  tgpconncomp  22655  prdstgpd  22667  tsmsmhm  22688  tsmsadd  22689  tsmssub  22691  tgptsmscls  22692  tsmssplit  22694  tsmsxplem1  22695  tsmsxplem2  22696  cnmpt1vsca  22736  tlmtgp  22738  ustuqtoplem  22782  utopsnneip  22791  ressprdsds  22915  metuval  23093  nmfval2  23134  tngnm  23194  nmoeq0  23279  idnghm  23286  cnmpt1ds  23384  fsumcn  23412  expcn  23414  divccn  23415  divccncf  23448  negcncf  23460  copco  23556  pcopt  23560  pcopt2  23561  pcoass  23562  pi1xfrcnvlem  23594  cnmpt1ip  23784  rrxnm  23928  rrxds  23930  minveclem3b  23965  divcncf  23982  ovolctb  24025  ovoliunnul  24042  voliunlem3  24087  ovolfs2  24106  uniioombllem2  24118  vitalilem4  24146  vitalilem5  24147  ismbf  24163  mbfss  24181  mbfmulc2re  24183  mbfneg  24185  mbfpos  24186  mbfposb  24188  mbfadd  24196  mbfsub  24197  mbfmulc2  24198  mbfinf  24200  mbflimsup  24201  mbflimlem  24202  i1fpos  24241  i1fposd  24242  itg1climres  24249  mbfmul  24261  itg2mulc  24282  itg2i1fseq  24290  itg2cnlem1  24296  itg2cnlem2  24297  itgresr  24313  iblneg  24337  i1fibl  24342  itgitg1  24343  iblsub  24356  itgfsum  24361  itgmulc2lem1  24366  limcmpt  24415  limccnp  24423  limcco  24425  dvreslem  24441  dvres2lem  24442  dvidlem  24447  dvcnp2  24451  dvaddbr  24469  dvmulbr  24470  dvmulf  24474  dvcmulf  24476  dvcobr  24477  dvcof  24479  dvcjbr  24480  dvcj  24481  dvfre  24482  dvexp  24484  dvexp2  24485  dvrec  24486  dvmptcmul  24495  dvmptdivc  24496  dvmptneg  24497  dvmptsub  24498  dvmptre  24500  dvmptim  24501  dvrecg  24504  dvmptdiv  24505  dvmptfsum  24506  dvcnvlem  24507  dvcnv  24508  dvexp3  24509  dvef  24511  dvsincos  24512  dv11cn  24532  lhop2  24546  lhop  24547  ftc2  24575  itgparts  24578  itgsubstlem  24579  mdegfval  24590  mdegmullem  24606  ply1termlem  24727  plypow  24729  plyconst  24730  plyeq0lem  24734  plypf1  24736  plyaddlem1  24737  plymullem1  24738  coeeulem  24748  coeidlem  24761  plyco  24765  coeeq2  24766  0dgr  24769  0dgrb  24770  dgrcolem1  24797  dgrcolem2  24798  plycjlem  24800  dvply1  24807  dvply2g  24808  plydiveu  24821  plyremlem  24827  elqaalem3  24844  taylfval  24881  dvtaylp  24892  taylthlem1  24895  taylthlem2  24896  ulmshft  24912  mtestbdd  24927  iblulm  24929  itgulm2  24931  pserulm  24944  psercn2  24945  pserdvlem2  24950  pserdv  24951  pserdv2  24952  abelthlem1  24953  abelthlem3  24955  advlog  25169  advlogexp  25170  dvcxp1  25253  dvcxp2  25254  dvcncxp1  25256  sqrtcn  25263  loglesqrt  25271  dvatan  25445  atantayl2  25448  atantayl3  25449  leibpi  25453  rlimcnp2  25477  efrlim  25480  dfef2  25481  cxp2lim  25487  divsqrtsumlem  25490  lgamgulmlem2  25540  lgamgulm2  25546  lgamcvglem  25550  gamcvg2lem  25569  ftalem7  25589  basellem9  25599  muinv  25703  logfacrlim  25733  logexprlim  25734  dchrmulid2  25761  dchrinvcl  25762  lgseisenlem3  25886  lgseisenlem4  25887  chtppilimlem2  25983  chebbnd2  25986  chpchtlim  25988  chpo1ub  25989  rpvmasumlem  25996  dchrmusumlema  26002  dchrvmasumlem1  26004  dchrvmasumiflem2  26011  dchrisum0fno1  26020  rpvmasum2  26021  dchrisum0lema  26023  dchrisum0lem1  26025  dchrisum0lem2a  26026  dchrisum0lem2  26027  dchrisum0  26029  dchrmusumlem  26031  dchrvmasumlem  26032  rpvmasum  26035  rplogsum  26036  logdivsum  26042  mulog2sumlem3  26045  vmalogdivsum2  26047  vmalogdivsum  26048  2vmadivsumlem  26049  logsqvma2  26052  log2sumbnd  26053  selberglem2  26055  selberg3lem1  26066  selberg3  26068  selberg4lem1  26069  selberg4  26070  pntrsumo1  26074  selberg3r  26078  selberg4r  26079  selberg34r  26080  pntrlog2bndlem2  26087  pntrlog2bndlem4  26089  pntrlog2bndlem5  26090  pntrlog2bndlem6  26092  padicabvf  26140  padicabvcxp  26141  mirval  26374  crctcshlem4  27531  clwlknf1oclwwlkn  27796  eucrct2eupth  27957  chscllem4  29350  brafnmul  29661  kbmul  29665  cofmpt2  30313  ofresid  30323  ofoprabco  30343  fcobijfs  30391  gsummpt2d  30620  gsummptres  30623  fzto1st1  30677  fzto1st  30678  freshmansdream  30792  lbsdiflsp0  30927  fedgmullem1  30930  fedgmullem2  30931  mdetpmtr1  30993  mdetlap  31002  xrge0mulc1cn  31089  esumval  31210  esumsnf  31228  esumpcvgval  31242  esumcvg  31250  esumcvgsum  31252  esumsup  31253  ofcfeqd2  31265  meascnbl  31383  sitgval  31495  probmeasb  31593  cndprobprob  31601  dstfrvclim1  31640  ballotlemfval  31652  ballotlemsval  31671  ballotlemieq  31679  plymul02  31721  plymulx0  31722  plymulx  31723  signsplypnf  31725  signstfv  31738  signstfvn  31744  signstfvp  31746  itgexpif  31782  logdivsqrle  31826  ptpconn  32383  cvmliftlem6  32440  cvmliftphtlem  32467  cvmlift3lem5  32473  elmrsubrn  32670  msubfval  32674  msubco  32681  divcnvlin  32867  knoppcnlem9  33743  knoppcnlem10  33744  knoppcnlem11  33745  bj-finsumval0  34461  curf  34756  matunitlindflem1  34774  matunitlindflem2  34775  poimirlem3  34781  poimirlem15  34793  poimirlem16  34794  poimirlem17  34795  poimirlem19  34797  poimirlem20  34798  broucube  34812  ovoliunnfl  34820  voliunnfl  34822  volsupnfl  34823  mbfposadd  34825  itg2addnclem  34829  itg2addnclem3  34831  itg2addnc  34832  itgaddnclem2  34837  itgaddnc  34838  iblsubnc  34839  itgsubnc  34840  itgmulc2nclem1  34844  itgmulc2nclem2  34845  itgmulc2nc  34846  itgabsnc  34847  ftc1cnnclem  34851  ftc1anclem3  34855  ftc1anclem5  34857  ftc1anclem6  34858  ftc1anclem8  34860  ftc1anc  34861  ftc2nc  34862  areacirclem1  34868  areacirclem2  34869  areacirclem4  34871  areacirc  34873  upixp  34891  qsalrel  39009  mzpsubst  39229  mzprename  39230  mzpcompact2lem  39232  eldioph2  39243  rabdiophlem2  39283  mendlmod  39677  mendassa  39678  areaquad  39707  fsovcnvlem  40243  hashnzfzclim  40538  expgrowthi  40549  expgrowth  40551  uzmptshftfval  40562  dvradcnv2  40563  binomcxplemrat  40566  binomcxplemfrat  40567  binomcxplemradcnv  40568  binomcxplemdvbinom  40569  binomcxplemcvg  40570  binomcxplemdvsum  40571  binomcxplemnotnn0  40572  mulc1cncfg  41754  expcnfg  41756  fprodcnlem  41764  clim1fr1  41766  divcnvg  41792  sublimc  41817  reclimc  41818  divlimc  41821  limsupresico  41865  limsuppnfdlem  41866  limsupvaluz  41873  supcnvlimsupmpt  41906  liminfresico  41936  climliminflimsupd  41966  cncfmptssg  42037  negcncfg  42048  cncficcgt0  42055  fprodcncf  42068  fprodsubrecnncnvlem  42075  fprodaddrecnncnvlem  42077  dvsinax  42081  dvasinbx  42089  dvdivf  42091  ioodvbdlimc1lem2  42101  ioodvbdlimc2lem  42103  dvnmptdivc  42107  dvxpaek  42109  dvnxpaek  42111  dvnmul  42112  dvnprodlem2  42116  ibliccsinexp  42120  itgsinexplem1  42123  itgsinexp  42124  iblempty  42134  itgcoscmulx  42138  itgsincmulx  42143  itgioocnicc  42146  iblcncfioo  42147  itgsbtaddcnst  42151  volioofmpt  42164  volicofmpt  42167  stoweidlem4  42174  stirlinglem5  42248  dirkerval  42261  dirkertrigeq  42271  dirkeritg  42272  dirkercncflem2  42274  dirkercncflem4  42276  fourierdlem16  42293  fourierdlem18  42295  fourierdlem21  42298  fourierdlem22  42299  fourierdlem28  42305  fourierdlem39  42316  fourierdlem40  42317  fourierdlem41  42318  fourierdlem53  42329  fourierdlem56  42332  fourierdlem57  42333  fourierdlem60  42336  fourierdlem61  42337  fourierdlem68  42344  fourierdlem73  42349  fourierdlem74  42350  fourierdlem75  42351  fourierdlem76  42352  fourierdlem78  42354  fourierdlem81  42357  fourierdlem82  42358  fourierdlem83  42359  fourierdlem84  42360  fourierdlem85  42361  fourierdlem88  42364  fourierdlem90  42366  fourierdlem92  42368  fourierdlem93  42369  fourierdlem95  42371  fourierdlem97  42373  fourierdlem101  42377  fourierdlem103  42379  fourierdlem104  42380  fourierdlem111  42387  fourierdlem112  42388  sqwvfoura  42398  sqwvfourb  42399  fouriersw  42401  elaa2lem  42403  etransclem4  42408  etransclem17  42421  etransclem18  42422  etransclem32  42436  etransclem46  42450  sge0z  42542  sge0revalmpt  42545  sge0tsms  42547  sge0sup  42558  sge0iunmptlemre  42582  sge0iun  42586  sge0xaddlem2  42601  ismeannd  42634  psmeasurelem  42637  meaiuninclem  42647  meaiininclem  42653  caratheodory  42695  isomenndlem  42697  ovnval  42708  hoicvrrex  42723  ovnlecvr  42725  ovncvrrp  42731  ovn0lem  42732  ovnsubaddlem1  42737  hoidmv1lelem2  42759  hoidmv1le  42761  hoidmvlelem3  42764  ovnhoilem2  42769  ovnhoi  42770  ovnlecvr2  42777  ovncvr2  42778  hspmbllem2  42794  ovolval2lem  42810  ovolval3  42814  ovolval5lem1  42819  ovolval5lem2  42820  ovnovollem1  42823  ovnovollem2  42824  vonioolem1  42847  vonicclem1  42850  vonct  42860  smflim  42938  smfinflem  42976  smflimsuplem5  42983  smfliminflem  42989  smndex1gid  43977  smndex1igid  43978  fdmdifeqresdif  44292  ply1mulgsumlem2  44343  lincvalsc0  44378  linc0scn0  44380  lincdifsn  44381  lincsum  44386  lincscm  44387  lindslinindimp2lem4  44418  lindslinindsimp2lem5  44419  lincresunit3lem2  44437  aacllem  44804  amgmwlem  44805
  Copyright terms: Public domain W3C validator