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

Theorem mpteq2dva 4714
 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 1840 . 2 𝑥𝜑
2 mpteq2dva.1 . 2 ((𝜑𝑥𝐴) → 𝐵 = 𝐶)
31, 2mpteq2da 4713 1 (𝜑 → (𝑥𝐴𝐵) = (𝑥𝐴𝐶))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 384   = wceq 1480   ∈ wcel 1987   ↦ cmpt 4683 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-ral 2913  df-opab 4684  df-mpt 4685 This theorem is referenced by:  mpteq2dv  4715  2fvcoidd  6517  offval  6869  offval2  6879  caofinvl  6889  caofcom  6894  caofass  6896  caofdi  6898  caofdir  6899  caonncan  6900  curry1  7229  curry2  7232  mpt2curryd  7355  pw2f1olem  8024  mapxpen  8086  xpmapenlem  8087  cantnfp1  8538  cantnflem1d  8545  cantnflem1  8546  cnfcom2lem  8558  dfac12lem1  8925  seqof  12814  seqof2  12815  swrd0val  13375  swrdswrd  13414  repswswrd  13484  repswrevw  13486  revco  13533  ccatco  13534  repsco  13538  ofccat  13658  lo1eq  14249  rlimeq  14250  lo1mul2  14309  o1dif  14310  lo1sub  14311  rlimdiv  14326  caucvgr  14356  sumeq1  14369  fsumrlim  14489  fsumo1  14490  climfsum  14498  geomulcvg  14551  vdwlem8  15635  prmgapprmo  15709  restid2  16031  pwsplusgval  16090  pwsmulrval  16091  pwsvscafval  16094  qusin  16144  xpsaddlem  16175  xpsvsca  16179  catidd  16281  fuclid  16566  fucrid  16567  fucass  16568  setcepi  16678  prf1st  16784  prf2nd  16785  1st2ndprf  16786  curfcl  16812  curfuncf  16818  diag2  16825  curf2ndf  16827  hof2val  16836  hofcllem  16838  hofcl  16839  yonedalem4a  16855  yonedalem4c  16857  yonedalem3b  16859  yonedainv  16861  yonffthlem  16862  prdsidlem  17262  prdsmndd  17263  pwsco2mhm  17311  frmdup3lem  17343  frmdup3  17344  grpinvpropd  17430  prdsinvlem  17464  pwsinvg  17468  pwssub  17469  galactghm  17763  cayleylem1  17772  pmtrprfval  17847  sylow1lem2  17954  sylow3lem1  17982  efginvrel1  18081  frgpup3lem  18130  frgpup3  18131  prdscmnd  18204  iscyggen  18222  gsumval3  18248  gsumcllem  18249  gsumzsplit  18267  gsumsub  18288  gsummptf1o  18302  gsum2d  18311  gsum2d2  18313  gsumxp  18315  prdsgsum  18317  telgsumfz  18327  telgsumfz0  18329  telgsum  18331  dprdfsub  18360  dprdfeq0  18361  dprddisj2  18378  dprd2d2  18383  dpjidcl  18397  ablfaclem2  18425  ablfac2  18428  srgbinomlem3  18482  srgbinomlem4  18483  srgbinomlem  18484  gsumdixp  18549  prdsmgp  18550  prdsringd  18552  prdslmodd  18909  asclpropd  19286  psrass1lem  19317  psrlinv  19337  psrass1  19345  psrdi  19346  psrdir  19347  psrass23l  19348  psrcom  19349  psrass23  19350  resspsrmul  19357  mplsubrglem  19379  mplmonmul  19404  mplcoe1  19405  mplcoe5  19408  mplcoe4  19443  evlslem3  19454  evlslem1  19455  psrplusgpropd  19546  psropprmul  19548  coe1mul2  19579  coe1tm  19583  coe1tmmul2  19586  coe1tmmul  19587  coe1pwmul  19589  cply1mul  19604  ply1coe  19606  eqcoe1ply1eq  19607  lply1binomsc  19617  evl1gsummon  19669  mulgrhm2  19787  frgpcyg  19862  evpmodpmf1o  19882  phlpropd  19940  frlmphl  20060  uvcresum  20072  frlmup1  20077  mamures  20136  grpvrinv  20142  mhmvlin  20143  mamuass  20148  mamudi  20149  mamudir  20150  mamuvs1  20151  mamuvs2  20152  mpt2matmul  20192  mamutpos  20204  madetsumid  20207  dmatmul  20243  scmatscm  20259  1mavmul  20294  mavmulass  20295  mvmumamul1  20300  mulmarep1gsum1  20319  mulmarep1gsum2  20320  mdetleib2  20334  mdetfval1  20336  mdet0pr  20338  mdetdiag  20345  mdetdiagid  20346  mdetrlin  20348  mdetrsca  20349  mdetralt  20354  mdetunilem9  20366  gsummatr01  20405  smadiadetlem1a  20409  smadiadetlem3  20414  smadiadetlem4  20415  cpmatmcllem  20463  mat2pmatmul  20476  decpmatmullem  20516  decpmatmul  20517  pmatcollpw1lem2  20520  pmatcollpw  20526  pmatcollpw3lem  20528  pmatcollpwscmat  20536  idpm2idmp  20546  mp2pm2mplem3  20553  mp2pm2mplem4  20554  mp2pm2mplem5  20555  mp2pm2mp  20556  pm2mpghm  20561  pm2mpmhmlem2  20564  monmat2matmon  20569  pm2mp  20570  chpdmat  20586  chpscmat  20587  chpscmatgsumbin  20589  chpscmatgsummon  20590  chp0mat  20591  chpidmat  20592  chfacfscmulgsum  20605  chfacfpmmulgsum  20609  chfacfpmmulgsum2  20610  cayhamlem1  20611  cpmidgsumm2pm  20614  cpmidpmat  20618  cpmadugsumlemB  20619  cpmadugsumlemC  20620  cpmadugsumlemF  20621  cpmadumatpoly  20628  cayhamlem3  20632  cayhamlem4  20633  cayleyhamilton0  20634  cayleyhamiltonALT  20636  neiptopnei  20876  neiptopreu  20877  ptcnplem  21364  cnmpt1t  21408  cnmpt12  21410  cnmptkp  21423  cnmptk1  21424  cnmpt1k  21425  cnmptkk  21426  cnmptk1p  21428  cnmpt2k  21431  qtopeu  21459  pt1hmeo  21549  ptunhmeo  21551  xkocnv  21557  xkohmeo  21558  flfcnp2  21751  cnmpt1plusg  21831  istgp2  21835  tmdmulg  21836  tgpmulg  21837  tmdgsum  21839  symgtgp  21845  subgtgp  21849  tgpconncomp  21856  prdstgpd  21868  tsmsmhm  21889  tsmsadd  21890  tsmssub  21892  tgptsmscls  21893  tsmssplit  21895  tsmsxplem1  21896  tsmsxplem2  21897  cnmpt1vsca  21937  tlmtgp  21939  ustuqtoplem  21983  utopsnneip  21992  ressprdsds  22116  metuval  22294  nmfval2  22335  tngnm  22395  nmoeq0  22480  idnghm  22487  cnmpt1ds  22585  fsumcn  22613  expcn  22615  divccn  22616  divccncf  22649  negcncf  22661  copco  22758  pcopt  22762  pcopt2  22763  pcoass  22764  pi1xfrcnvlem  22796  cnmpt1ip  22986  rrxnm  23119  rrxds  23121  minveclem3b  23139  divcncf  23156  ovolctb  23198  ovoliunnul  23215  voliunlem3  23260  ovolfs2  23279  uniioombllem2  23291  vitalilem4  23320  vitalilem5  23321  ismbf  23337  mbfss  23353  mbfmulc2re  23355  mbfneg  23357  mbfpos  23358  mbfposb  23360  mbfadd  23368  mbfsub  23369  mbfmulc2  23370  mbfinf  23372  mbflimsup  23373  mbflimlem  23374  i1fpos  23413  i1fposd  23414  itg1climres  23421  mbfmul  23433  itg2mulc  23454  itg2i1fseq  23462  itg2cnlem1  23468  itg2cnlem2  23469  itgresr  23485  iblneg  23509  i1fibl  23514  itgitg1  23515  iblsub  23528  itgfsum  23533  itgmulc2lem1  23538  limcmpt  23587  limccnp  23595  limcco  23597  dvreslem  23613  dvres2lem  23614  dvidlem  23619  dvcnp2  23623  dvaddbr  23641  dvmulbr  23642  dvmulf  23646  dvcmulf  23648  dvcobr  23649  dvcof  23651  dvcjbr  23652  dvcj  23653  dvfre  23654  dvexp  23656  dvexp2  23657  dvrec  23658  dvmptcmul  23667  dvmptdivc  23668  dvmptneg  23669  dvmptsub  23670  dvmptre  23672  dvmptim  23673  dvmptfsum  23676  dvcnvlem  23677  dvcnv  23678  dvexp3  23679  dvef  23681  dvsincos  23682  dv11cn  23702  lhop2  23716  lhop  23717  ftc2  23745  itgparts  23748  itgsubstlem  23749  mdegfval  23760  mdegmullem  23776  ply1termlem  23897  plypow  23899  plyconst  23900  plyeq0lem  23904  plypf1  23906  plyaddlem1  23907  plymullem1  23908  coeeulem  23918  coeidlem  23931  plyco  23935  coeeq2  23936  0dgr  23939  0dgrb  23940  dgrcolem1  23967  dgrcolem2  23968  plycjlem  23970  dvply1  23977  dvply2g  23978  plydiveu  23991  plyremlem  23997  elqaalem3  24014  taylfval  24051  dvtaylp  24062  taylthlem1  24065  taylthlem2  24066  ulmshft  24082  mtestbdd  24097  iblulm  24099  itgulm2  24101  pserulm  24114  psercn2  24115  pserdvlem2  24120  pserdv  24121  pserdv2  24122  abelthlem1  24123  abelthlem3  24125  advlog  24334  advlogexp  24335  dvcxp1  24415  dvcxp2  24416  dvcncxp1  24418  sqrtcn  24425  loglesqrt  24433  dvatan  24596  atantayl2  24599  atantayl3  24600  leibpi  24603  rlimcnp2  24627  efrlim  24630  dfef2  24631  cxp2lim  24637  divsqrtsumlem  24640  lgamgulmlem2  24690  lgamgulm2  24696  lgamcvglem  24700  gamcvg2lem  24719  ftalem7  24739  basellem9  24749  muinv  24853  logfacrlim  24883  logexprlim  24884  dchrmulid2  24911  dchrinvcl  24912  lgseisenlem3  25036  lgseisenlem4  25037  chtppilimlem2  25097  chebbnd2  25100  chpchtlim  25102  chpo1ub  25103  rpvmasumlem  25110  dchrmusumlema  25116  dchrvmasumlem1  25118  dchrvmasumiflem2  25125  dchrisum0fno1  25134  rpvmasum2  25135  dchrisum0lema  25137  dchrisum0lem1  25139  dchrisum0lem2a  25140  dchrisum0lem2  25141  dchrisum0  25143  dchrmusumlem  25145  dchrvmasumlem  25146  rpvmasum  25149  rplogsum  25150  logdivsum  25156  mulog2sumlem3  25159  vmalogdivsum2  25161  vmalogdivsum  25162  2vmadivsumlem  25163  logsqvma2  25166  log2sumbnd  25167  selberglem2  25169  selberg3lem1  25180  selberg3  25182  selberg4lem1  25183  selberg4  25184  pntrsumo1  25188  selberg3r  25192  selberg4r  25193  selberg34r  25194  pntrlog2bndlem2  25201  pntrlog2bndlem4  25203  pntrlog2bndlem5  25204  pntrlog2bndlem6  25206  padicabvf  25254  padicabvcxp  25255  mirval  25484  crctcshlem4  26615  eucrct2eupth  27005  chscllem4  28387  brafnmul  28698  kbmul  28702  ofresid  29327  ofoprabco  29348  fcobijfs  29385  gsummpt2d  29608  gsummptres  29611  fzto1st1  29679  fzto1st  29680  mdetpmtr1  29713  mdetlap  29722  xrge0mulc1cn  29811  esumval  29931  esumsnf  29949  esumpcvgval  29963  esumcvg  29971  esumcvgsum  29973  esumsup  29974  ofcfeqd2  29986  meascnbl  30105  sitgval  30217  probmeasb  30315  cndprobprob  30323  dstfrvclim1  30362  ballotlemfval  30374  ballotlemsval  30393  ballotlemieq  30401  plymul02  30445  plymulx0  30446  plymulx  30447  signsplypnf  30449  signstfv  30462  signstfvn  30468  signstfvp  30470  itgexpif  30493  ptpconn  30976  cvmliftlem6  31033  cvmliftphtlem  31060  cvmlift3lem5  31066  elmrsubrn  31178  msubfval  31182  msubco  31189  divcnvlin  31379  knoppcnlem9  32186  knoppcnlem10  32187  knoppcnlem11  32188  bj-finsumval0  32819  curf  33058  matunitlindflem1  33076  matunitlindflem2  33077  poimirlem3  33083  poimirlem15  33095  poimirlem16  33096  poimirlem17  33097  poimirlem19  33099  poimirlem20  33100  broucube  33114  ovoliunnfl  33122  voliunnfl  33124  volsupnfl  33125  mbfposadd  33128  itg2addnclem  33132  itg2addnclem3  33134  itg2addnc  33135  itgaddnclem2  33140  itgaddnc  33141  iblsubnc  33142  itgsubnc  33143  itgmulc2nclem1  33147  itgmulc2nclem2  33148  itgmulc2nc  33149  itgabsnc  33150  ftc1cnnclem  33154  ftc1anclem3  33158  ftc1anclem5  33160  ftc1anclem6  33161  ftc1anclem8  33163  ftc1anc  33164  ftc2nc  33165  areacirclem1  33171  areacirclem2  33172  areacirclem4  33174  areacirc  33176  upixp  33195  mzpsubst  36830  mzprename  36831  mzpcompact2lem  36833  eldioph2  36844  rabdiophlem2  36885  mendlmod  37283  mendassa  37284  areaquad  37322  fsovcnvlem  37828  hashnzfzclim  38042  expgrowthi  38053  expgrowth  38055  uzmptshftfval  38066  dvradcnv2  38067  binomcxplemrat  38070  binomcxplemfrat  38071  binomcxplemradcnv  38072  binomcxplemdvbinom  38073  binomcxplemcvg  38074  binomcxplemdvsum  38075  binomcxplemnotnn0  38076  mulc1cncfg  39257  expcnfg  39259  fprodcnlem  39267  clim1fr1  39269  divcnvg  39295  sublimc  39320  reclimc  39321  divlimc  39324  limsupresico  39368  limsuppnfdlem  39369  limsupvaluz  39376  supcnvlimsupmpt  39409  cncfmptssg  39418  negcncfg  39429  cncficcgt0  39436  fprodcncf  39449  fprodsubrecnncnvlem  39456  fprodaddrecnncnvlem  39458  dvrecg  39462  dvsinax  39463  dvmptdiv  39469  dvasinbx  39472  dvdivf  39474  ioodvbdlimc1lem2  39484  ioodvbdlimc2lem  39486  dvnmptdivc  39490  dvxpaek  39492  dvnxpaek  39494  dvnmul  39495  dvnprodlem2  39499  ibliccsinexp  39503  itgsinexplem1  39506  itgsinexp  39507  iblempty  39518  itgcoscmulx  39522  itgsincmulx  39527  itgioocnicc  39530  iblcncfioo  39531  itgsbtaddcnst  39535  volioofmpt  39548  volicofmpt  39551  stoweidlem4  39558  stirlinglem5  39632  dirkerval  39645  dirkertrigeq  39655  dirkeritg  39656  dirkercncflem2  39658  dirkercncflem4  39660  fourierdlem16  39677  fourierdlem18  39679  fourierdlem21  39682  fourierdlem22  39683  fourierdlem28  39689  fourierdlem39  39700  fourierdlem40  39701  fourierdlem41  39702  fourierdlem53  39713  fourierdlem56  39716  fourierdlem57  39717  fourierdlem60  39720  fourierdlem61  39721  fourierdlem68  39728  fourierdlem73  39733  fourierdlem74  39734  fourierdlem75  39735  fourierdlem76  39736  fourierdlem78  39738  fourierdlem81  39741  fourierdlem82  39742  fourierdlem83  39743  fourierdlem84  39744  fourierdlem85  39745  fourierdlem88  39748  fourierdlem90  39750  fourierdlem92  39752  fourierdlem93  39753  fourierdlem95  39755  fourierdlem97  39757  fourierdlem101  39761  fourierdlem103  39763  fourierdlem104  39764  fourierdlem111  39771  fourierdlem112  39772  sqwvfoura  39782  sqwvfourb  39783  fouriersw  39785  elaa2lem  39787  etransclem4  39792  etransclem17  39805  etransclem18  39806  etransclem32  39820  etransclem46  39834  sge0z  39929  sge0revalmpt  39932  sge0tsms  39934  sge0sup  39945  sge0iunmptlemre  39969  sge0iun  39973  sge0xaddlem2  39988  ismeannd  40021  psmeasurelem  40024  meaiuninclem  40034  meaiininclem  40037  caratheodory  40079  isomenndlem  40081  ovnval  40092  hoicvrrex  40107  ovnlecvr  40109  ovncvrrp  40115  ovn0lem  40116  ovnsubaddlem1  40121  hoidmv1lelem2  40143  hoidmv1le  40145  hoidmvlelem3  40148  ovnhoilem2  40153  ovnhoi  40154  ovnlecvr2  40161  ovncvr2  40162  hspmbllem2  40178  ovolval2lem  40194  ovolval3  40198  ovolval5lem1  40203  ovolval5lem2  40204  ovnovollem1  40207  ovnovollem2  40208  vonioolem1  40231  vonicclem1  40234  vonct  40244  smflim  40322  smfinflem  40360  smflimsuplem5  40367  fdmdifeqresdif  41438  ply1mulgsumlem2  41493  lincvalsc0  41528  linc0scn0  41530  lincdifsn  41531  lincsum  41536  lincscm  41537  lindslinindimp2lem4  41568  lindslinindsimp2lem5  41569  lincresunit3lem2  41587  aacllem  41880  amgmwlem  41881
 Copyright terms: Public domain W3C validator