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

Theorem mpteq2dva 4777
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 1883 . 2 𝑥𝜑
2 mpteq2dva.1 . 2 ((𝜑𝑥𝐴) → 𝐵 = 𝐶)
31, 2mpteq2da 4776 1 (𝜑 → (𝑥𝐴𝐵) = (𝑥𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1523  wcel 2030  cmpt 4762
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-ral 2946  df-opab 4746  df-mpt 4763
This theorem is referenced by:  mpteq2dv  4778  2fvcoidd  6592  offval  6946  offval2  6956  caofinvl  6966  caofcom  6971  caofass  6973  caofdi  6975  caofdir  6976  caonncan  6977  curry1  7314  curry2  7317  mpt2curryd  7440  pw2f1olem  8105  mapxpen  8167  xpmapenlem  8168  cantnfp1  8616  cantnflem1d  8623  cantnflem1  8624  cnfcom2lem  8636  dfac12lem1  9003  seqof  12898  seqof2  12899  swrd0val  13466  swrdswrd  13506  repswswrd  13577  repswrevw  13579  revco  13626  ccatco  13627  repsco  13631  ofccat  13754  lo1eq  14343  rlimeq  14344  lo1mul2  14403  o1dif  14404  lo1sub  14405  rlimdiv  14420  caucvgr  14450  sumeq1  14463  fsumrlim  14587  fsumo1  14588  climfsum  14596  geomulcvg  14651  vdwlem8  15739  prmgapprmo  15813  restid2  16138  pwsplusgval  16197  pwsmulrval  16198  pwsvscafval  16201  qusin  16251  xpsaddlem  16282  xpsvsca  16286  catidd  16388  fuclid  16673  fucrid  16674  fucass  16675  setcepi  16785  prf1st  16891  prf2nd  16892  1st2ndprf  16893  curfcl  16919  curfuncf  16925  diag2  16932  curf2ndf  16934  hof2val  16943  hofcllem  16945  hofcl  16946  yonedalem4a  16962  yonedalem4c  16964  yonedalem3b  16966  yonedainv  16968  yonffthlem  16969  prdsidlem  17369  prdsmndd  17370  pwsco2mhm  17418  frmdup3lem  17450  frmdup3  17451  grpinvpropd  17537  prdsinvlem  17571  pwsinvg  17575  pwssub  17576  galactghm  17869  cayleylem1  17878  pmtrprfval  17953  sylow1lem2  18060  sylow3lem1  18088  efginvrel1  18187  frgpup3lem  18236  frgpup3  18237  prdscmnd  18310  iscyggen  18328  gsumval3  18354  gsumcllem  18355  gsumzsplit  18373  gsumsub  18394  gsummptf1o  18408  gsum2d  18417  gsum2d2  18419  gsumxp  18421  prdsgsum  18423  telgsumfz  18433  telgsumfz0  18435  telgsum  18437  dprdfsub  18466  dprdfeq0  18467  dprddisj2  18484  dprd2d2  18489  dpjidcl  18503  ablfaclem2  18531  ablfac2  18534  srgbinomlem3  18588  srgbinomlem4  18589  srgbinomlem  18590  gsumdixp  18655  prdsmgp  18656  prdsringd  18658  prdslmodd  19017  asclpropd  19394  psrass1lem  19425  psrlinv  19445  psrass1  19453  psrdi  19454  psrdir  19455  psrass23l  19456  psrcom  19457  psrass23  19458  resspsrmul  19465  mplsubrglem  19487  mplmonmul  19512  mplcoe1  19513  mplcoe5  19516  mplcoe4  19551  evlslem3  19562  evlslem1  19563  psrplusgpropd  19654  psropprmul  19656  coe1mul2  19687  coe1tm  19691  coe1tmmul2  19694  coe1tmmul  19695  coe1pwmul  19697  cply1mul  19712  ply1coe  19714  eqcoe1ply1eq  19715  lply1binomsc  19725  evl1gsummon  19777  mulgrhm2  19895  frgpcyg  19970  evpmodpmf1o  19990  phlpropd  20048  frlmphl  20168  uvcresum  20180  frlmup1  20185  mamures  20244  grpvrinv  20250  mhmvlin  20251  mamuass  20256  mamudi  20257  mamudir  20258  mamuvs1  20259  mamuvs2  20260  mpt2matmul  20300  mamutpos  20312  madetsumid  20315  dmatmul  20351  scmatscm  20367  1mavmul  20402  mavmulass  20403  mvmumamul1  20408  mulmarep1gsum1  20427  mulmarep1gsum2  20428  mdetleib2  20442  mdetfval1  20444  mdet0pr  20446  mdetdiag  20453  mdetdiagid  20454  mdetrlin  20456  mdetrsca  20457  mdetralt  20462  mdetunilem9  20474  gsummatr01  20513  smadiadetlem1a  20517  smadiadetlem3  20522  smadiadetlem4  20523  cpmatmcllem  20571  mat2pmatmul  20584  decpmatmullem  20624  decpmatmul  20625  pmatcollpw1lem2  20628  pmatcollpw  20634  pmatcollpw3lem  20636  pmatcollpwscmat  20644  idpm2idmp  20654  mp2pm2mplem3  20661  mp2pm2mplem4  20662  mp2pm2mplem5  20663  mp2pm2mp  20664  pm2mpghm  20669  pm2mpmhmlem2  20672  monmat2matmon  20677  pm2mp  20678  chpdmat  20694  chpscmat  20695  chpscmatgsumbin  20697  chpscmatgsummon  20698  chp0mat  20699  chpidmat  20700  chfacfscmulgsum  20713  chfacfpmmulgsum  20717  chfacfpmmulgsum2  20718  cayhamlem1  20719  cpmidgsumm2pm  20722  cpmidpmat  20726  cpmadugsumlemB  20727  cpmadugsumlemC  20728  cpmadugsumlemF  20729  cpmadumatpoly  20736  cayhamlem3  20740  cayhamlem4  20741  cayleyhamilton0  20742  cayleyhamiltonALT  20744  neiptopnei  20984  neiptopreu  20985  ptcnplem  21472  cnmpt1t  21516  cnmpt12  21518  cnmptkp  21531  cnmptk1  21532  cnmpt1k  21533  cnmptkk  21534  cnmptk1p  21536  cnmpt2k  21539  qtopeu  21567  pt1hmeo  21657  ptunhmeo  21659  xkocnv  21665  xkohmeo  21666  flfcnp2  21858  cnmpt1plusg  21938  istgp2  21942  tmdmulg  21943  tgpmulg  21944  tmdgsum  21946  symgtgp  21952  subgtgp  21956  tgpconncomp  21963  prdstgpd  21975  tsmsmhm  21996  tsmsadd  21997  tsmssub  21999  tgptsmscls  22000  tsmssplit  22002  tsmsxplem1  22003  tsmsxplem2  22004  cnmpt1vsca  22044  tlmtgp  22046  ustuqtoplem  22090  utopsnneip  22099  ressprdsds  22223  metuval  22401  nmfval2  22442  tngnm  22502  nmoeq0  22587  idnghm  22594  cnmpt1ds  22692  fsumcn  22720  expcn  22722  divccn  22723  divccncf  22756  negcncf  22768  copco  22864  pcopt  22868  pcopt2  22869  pcoass  22870  pi1xfrcnvlem  22902  cnmpt1ip  23092  rrxnm  23225  rrxds  23227  minveclem3b  23245  divcncf  23262  ovolctb  23304  ovoliunnul  23321  voliunlem3  23366  ovolfs2  23385  uniioombllem2  23397  vitalilem4  23425  vitalilem5  23426  ismbf  23442  mbfss  23458  mbfmulc2re  23460  mbfneg  23462  mbfpos  23463  mbfposb  23465  mbfadd  23473  mbfsub  23474  mbfmulc2  23475  mbfinf  23477  mbflimsup  23478  mbflimlem  23479  i1fpos  23518  i1fposd  23519  itg1climres  23526  mbfmul  23538  itg2mulc  23559  itg2i1fseq  23567  itg2cnlem1  23573  itg2cnlem2  23574  itgresr  23590  iblneg  23614  i1fibl  23619  itgitg1  23620  iblsub  23633  itgfsum  23638  itgmulc2lem1  23643  limcmpt  23692  limccnp  23700  limcco  23702  dvreslem  23718  dvres2lem  23719  dvidlem  23724  dvcnp2  23728  dvaddbr  23746  dvmulbr  23747  dvmulf  23751  dvcmulf  23753  dvcobr  23754  dvcof  23756  dvcjbr  23757  dvcj  23758  dvfre  23759  dvexp  23761  dvexp2  23762  dvrec  23763  dvmptcmul  23772  dvmptdivc  23773  dvmptneg  23774  dvmptsub  23775  dvmptre  23777  dvmptim  23778  dvrecg  23781  dvmptdiv  23782  dvmptfsum  23783  dvcnvlem  23784  dvcnv  23785  dvexp3  23786  dvef  23788  dvsincos  23789  dv11cn  23809  lhop2  23823  lhop  23824  ftc2  23852  itgparts  23855  itgsubstlem  23856  mdegfval  23867  mdegmullem  23883  ply1termlem  24004  plypow  24006  plyconst  24007  plyeq0lem  24011  plypf1  24013  plyaddlem1  24014  plymullem1  24015  coeeulem  24025  coeidlem  24038  plyco  24042  coeeq2  24043  0dgr  24046  0dgrb  24047  dgrcolem1  24074  dgrcolem2  24075  plycjlem  24077  dvply1  24084  dvply2g  24085  plydiveu  24098  plyremlem  24104  elqaalem3  24121  taylfval  24158  dvtaylp  24169  taylthlem1  24172  taylthlem2  24173  ulmshft  24189  mtestbdd  24204  iblulm  24206  itgulm2  24208  pserulm  24221  psercn2  24222  pserdvlem2  24227  pserdv  24228  pserdv2  24229  abelthlem1  24230  abelthlem3  24232  advlog  24445  advlogexp  24446  dvcxp1  24526  dvcxp2  24527  dvcncxp1  24529  sqrtcn  24536  loglesqrt  24544  dvatan  24707  atantayl2  24710  atantayl3  24711  leibpi  24714  rlimcnp2  24738  efrlim  24741  dfef2  24742  cxp2lim  24748  divsqrtsumlem  24751  lgamgulmlem2  24801  lgamgulm2  24807  lgamcvglem  24811  gamcvg2lem  24830  ftalem7  24850  basellem9  24860  muinv  24964  logfacrlim  24994  logexprlim  24995  dchrmulid2  25022  dchrinvcl  25023  lgseisenlem3  25147  lgseisenlem4  25148  chtppilimlem2  25208  chebbnd2  25211  chpchtlim  25213  chpo1ub  25214  rpvmasumlem  25221  dchrmusumlema  25227  dchrvmasumlem1  25229  dchrvmasumiflem2  25236  dchrisum0fno1  25245  rpvmasum2  25246  dchrisum0lema  25248  dchrisum0lem1  25250  dchrisum0lem2a  25251  dchrisum0lem2  25252  dchrisum0  25254  dchrmusumlem  25256  dchrvmasumlem  25257  rpvmasum  25260  rplogsum  25261  logdivsum  25267  mulog2sumlem3  25270  vmalogdivsum2  25272  vmalogdivsum  25273  2vmadivsumlem  25274  logsqvma2  25277  log2sumbnd  25278  selberglem2  25280  selberg3lem1  25291  selberg3  25293  selberg4lem1  25294  selberg4  25295  pntrsumo1  25299  selberg3r  25303  selberg4r  25304  selberg34r  25305  pntrlog2bndlem2  25312  pntrlog2bndlem4  25314  pntrlog2bndlem5  25315  pntrlog2bndlem6  25317  padicabvf  25365  padicabvcxp  25366  mirval  25595  crctcshlem4  26768  eucrct2eupth  27223  chscllem4  28627  brafnmul  28938  kbmul  28942  ofresid  29572  ofoprabco  29592  fcobijfs  29629  gsummpt2d  29909  gsummptres  29912  fzto1st1  29980  fzto1st  29981  mdetpmtr1  30017  mdetlap  30026  xrge0mulc1cn  30115  esumval  30236  esumsnf  30254  esumpcvgval  30268  esumcvg  30276  esumcvgsum  30278  esumsup  30279  ofcfeqd2  30291  meascnbl  30410  sitgval  30522  probmeasb  30620  cndprobprob  30628  dstfrvclim1  30667  ballotlemfval  30679  ballotlemsval  30698  ballotlemieq  30706  plymul02  30751  plymulx0  30752  plymulx  30753  signsplypnf  30755  signstfv  30768  signstfvn  30774  signstfvp  30776  itgexpif  30812  logdivsqrle  30856  ptpconn  31341  cvmliftlem6  31398  cvmliftphtlem  31425  cvmlift3lem5  31431  elmrsubrn  31543  msubfval  31547  msubco  31554  divcnvlin  31744  knoppcnlem9  32616  knoppcnlem10  32617  knoppcnlem11  32618  bj-finsumval0  33277  curf  33517  matunitlindflem1  33535  matunitlindflem2  33536  poimirlem3  33542  poimirlem15  33554  poimirlem16  33555  poimirlem17  33556  poimirlem19  33558  poimirlem20  33559  broucube  33573  ovoliunnfl  33581  voliunnfl  33583  volsupnfl  33584  mbfposadd  33587  itg2addnclem  33591  itg2addnclem3  33593  itg2addnc  33594  itgaddnclem2  33599  itgaddnc  33600  iblsubnc  33601  itgsubnc  33602  itgmulc2nclem1  33606  itgmulc2nclem2  33607  itgmulc2nc  33608  itgabsnc  33609  ftc1cnnclem  33613  ftc1anclem3  33617  ftc1anclem5  33619  ftc1anclem6  33620  ftc1anclem8  33622  ftc1anc  33623  ftc2nc  33624  areacirclem1  33630  areacirclem2  33631  areacirclem4  33633  areacirc  33635  upixp  33654  mzpsubst  37628  mzprename  37629  mzpcompact2lem  37631  eldioph2  37642  rabdiophlem2  37683  mendlmod  38080  mendassa  38081  areaquad  38119  fsovcnvlem  38624  hashnzfzclim  38838  expgrowthi  38849  expgrowth  38851  uzmptshftfval  38862  dvradcnv2  38863  binomcxplemrat  38866  binomcxplemfrat  38867  binomcxplemradcnv  38868  binomcxplemdvbinom  38869  binomcxplemcvg  38870  binomcxplemdvsum  38871  binomcxplemnotnn0  38872  mulc1cncfg  40139  expcnfg  40141  fprodcnlem  40149  clim1fr1  40151  divcnvg  40177  sublimc  40202  reclimc  40203  divlimc  40206  limsupresico  40250  limsuppnfdlem  40251  limsupvaluz  40258  supcnvlimsupmpt  40291  liminfresico  40321  climliminflimsupd  40351  cncfmptssg  40401  negcncfg  40412  cncficcgt0  40419  fprodcncf  40432  fprodsubrecnncnvlem  40439  fprodaddrecnncnvlem  40441  dvsinax  40445  dvasinbx  40453  dvdivf  40455  ioodvbdlimc1lem2  40465  ioodvbdlimc2lem  40467  dvnmptdivc  40471  dvxpaek  40473  dvnxpaek  40475  dvnmul  40476  dvnprodlem2  40480  ibliccsinexp  40484  itgsinexplem1  40487  itgsinexp  40488  iblempty  40499  itgcoscmulx  40503  itgsincmulx  40508  itgioocnicc  40511  iblcncfioo  40512  itgsbtaddcnst  40516  volioofmpt  40529  volicofmpt  40532  stoweidlem4  40539  stirlinglem5  40613  dirkerval  40626  dirkertrigeq  40636  dirkeritg  40637  dirkercncflem2  40639  dirkercncflem4  40641  fourierdlem16  40658  fourierdlem18  40660  fourierdlem21  40663  fourierdlem22  40664  fourierdlem28  40670  fourierdlem39  40681  fourierdlem40  40682  fourierdlem41  40683  fourierdlem53  40694  fourierdlem56  40697  fourierdlem57  40698  fourierdlem60  40701  fourierdlem61  40702  fourierdlem68  40709  fourierdlem73  40714  fourierdlem74  40715  fourierdlem75  40716  fourierdlem76  40717  fourierdlem78  40719  fourierdlem81  40722  fourierdlem82  40723  fourierdlem83  40724  fourierdlem84  40725  fourierdlem85  40726  fourierdlem88  40729  fourierdlem90  40731  fourierdlem92  40733  fourierdlem93  40734  fourierdlem95  40736  fourierdlem97  40738  fourierdlem101  40742  fourierdlem103  40744  fourierdlem104  40745  fourierdlem111  40752  fourierdlem112  40753  sqwvfoura  40763  sqwvfourb  40764  fouriersw  40766  elaa2lem  40768  etransclem4  40773  etransclem17  40786  etransclem18  40787  etransclem32  40801  etransclem46  40815  sge0z  40910  sge0revalmpt  40913  sge0tsms  40915  sge0sup  40926  sge0iunmptlemre  40950  sge0iun  40954  sge0xaddlem2  40969  ismeannd  41002  psmeasurelem  41005  meaiuninclem  41015  meaiininclem  41021  caratheodory  41063  isomenndlem  41065  ovnval  41076  hoicvrrex  41091  ovnlecvr  41093  ovncvrrp  41099  ovn0lem  41100  ovnsubaddlem1  41105  hoidmv1lelem2  41127  hoidmv1le  41129  hoidmvlelem3  41132  ovnhoilem2  41137  ovnhoi  41138  ovnlecvr2  41145  ovncvr2  41146  hspmbllem2  41162  ovolval2lem  41178  ovolval3  41182  ovolval5lem1  41187  ovolval5lem2  41188  ovnovollem1  41191  ovnovollem2  41192  vonioolem1  41215  vonicclem1  41218  vonct  41228  smflim  41306  smfinflem  41344  smflimsuplem5  41351  smfliminflem  41357  fdmdifeqresdif  42445  ply1mulgsumlem2  42500  lincvalsc0  42535  linc0scn0  42537  lincdifsn  42538  lincsum  42543  lincscm  42544  lindslinindimp2lem4  42575  lindslinindsimp2lem5  42576  lincresunit3lem2  42594  aacllem  42875  amgmwlem  42876
  Copyright terms: Public domain W3C validator