Theorem mpteq2dva 4969

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

Step	Hyp	Ref	Expression
1		nfv 2013	. 2 ⊢ Ⅎ𝑥𝜑
2		mpteq2dva.1	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)
3	1, 2	mpteq2da 4968	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))

Syntax hints:   → wi 4   ∧ wa 386   = wceq 1656   ∈ wcel 2164   ↦ cmpt 4954

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-ral 3122  df-opab 4938  df-mpt 4955

This theorem is referenced by:  mpteq2dv  4970  2fvcoidd  6812  offval  7169  offval2  7179  caofinvl  7189  caofcom  7194  caofass  7196  caofdi  7198  caofdir  7199  caonncan  7200  curry1  7538  curry2  7541  mpt2curryd  7665  pw2f1olem  8339  mapxpen  8401  xpmapenlem  8402  cantnfp1  8862  cantnflem1d  8869  cantnflem1  8870  cnfcom2lem  8882  dfac12lem1  9287  seqof  13159  seqof2  13160  swrd0valOLD  13714  swrdswrd  13791  repswswrd  13907  repswrevw  13910  revco  13962  ccatco  13963  repsco  13968  ofccat  14094  lo1eq  14683  rlimeq  14684  lo1mul2  14743  o1dif  14744  lo1sub  14745  rlimdiv  14760  caucvgr  14790  sumeq1  14803  fsumrlim  14924  fsumo1  14925  climfsum  14933  geomulcvg  14988  vdwlem8  16070  prmgapprmo  16144  restid2  16451  pwsplusgval  16510  pwsmulrval  16511  pwsvscafval  16514  qusin  16564  xpsaddlem  16595  xpsvsca  16599  catidd  16700  fuclid  16985  fucrid  16986  fucass  16987  setcepi  17097  prf1st  17204  prf2nd  17205  1st2ndprf  17206  curfcl  17232  curfuncf  17238  diag2  17245  curf2ndf  17247  hof2val  17256  hofcllem  17258  hofcl  17259  yonedalem4a  17275  yonedalem4c  17277  yonedalem3b  17279  yonedainv  17281  yonffthlem  17282  prdsidlem  17682  prdsmndd  17683  pwsco2mhm  17731  frmdup3lem  17764  frmdup3  17765  grpinvpropd  17851  prdsinvlem  17885  pwsinvg  17889  pwssub  17890  galactghm  18180  cayleylem1  18189  pmtrprfval  18264  sylow1lem2  18372  sylow3lem1  18400  efginvrel1  18499  frgpup3lem  18550  frgpup3  18551  prdscmnd  18624  iscyggen  18642  gsumval3  18668  gsumcllem  18669  gsumzsplit  18687  gsumsub  18708  gsummptf1o  18722  gsum2d  18731  gsum2d2  18733  gsumxp  18735  prdsgsum  18737  telgsumfz  18748  telgsumfz0  18750  telgsum  18752  dprdfsub  18781  dprdfeq0  18782  dprddisj2  18799  dprd2d2  18804  dpjidcl  18818  ablfaclem2  18846  ablfac2  18849  srgbinomlem3  18903  srgbinomlem4  18904  srgbinomlem  18905  gsumdixp  18970  prdsmgp  18971  prdsringd  18973  prdslmodd  19335  asclpropd  19714  psrass1lem  19745  psrlinv  19765  psrass1  19773  psrdi  19774  psrdir  19775  psrass23l  19776  psrcom  19777  psrass23  19778  resspsrmul  19785  mplsubrglem  19807  mplmonmul  19832  mplcoe1  19833  mplcoe5  19836  mplcoe4  19870  evlslem3  19881  evlslem1  19882  psrplusgpropd  19973  psropprmul  19975  coe1mul2  20006  coe1tm  20010  coe1tmmul2  20013  coe1tmmul  20014  coe1pwmul  20016  cply1mul  20031  ply1coe  20033  eqcoe1ply1eq  20034  lply1binomsc  20044  evl1gsummon  20096  mulgrhm2  20214  frgpcyg  20288  evpmodpmf1o  20309  phlpropd  20369  frlmphl  20494  uvcresum  20506  frlmup1  20511  mamures  20570  grpvrinv  20576  mhmvlin  20577  mamuass  20582  mamudi  20583  mamudir  20584  mamuvs1  20585  mamuvs2  20586  mpt2matmul  20627  mamutpos  20639  madetsumid  20642  dmatmul  20678  scmatscm  20694  1mavmul  20729  mavmulass  20730  mvmumamul1  20735  mulmarep1gsum1  20754  mulmarep1gsum2  20755  mdetleib2  20769  mdetfval1  20771  mdet0pr  20773  mdetdiag  20780  mdetdiagid  20781  mdetrlin  20783  mdetrsca  20784  mdetralt  20789  mdetunilem9  20801  gsummatr01  20841  smadiadetlem1a  20845  smadiadetlem3  20850  smadiadetlem4  20851  cpmatmcllem  20900  mat2pmatmul  20913  decpmatmullem  20953  decpmatmul  20954  pmatcollpw1lem2  20957  pmatcollpw  20963  pmatcollpw3lem  20965  pmatcollpwscmat  20973  idpm2idmp  20983  mp2pm2mplem3  20990  mp2pm2mplem4  20991  mp2pm2mplem5  20992  mp2pm2mp  20993  pm2mpghm  20998  pm2mpmhmlem2  21001  monmat2matmon  21006  pm2mp  21007  chpdmat  21023  chpscmat  21024  chpscmatgsumbin  21026  chpscmatgsummon  21027  chp0mat  21028  chpidmat  21029  chfacfscmulgsum  21042  chfacfpmmulgsum  21046  chfacfpmmulgsum2  21047  cayhamlem1  21048  cpmidgsumm2pm  21051  cpmidpmat  21055  cpmadugsumlemB  21056  cpmadugsumlemC  21057  cpmadugsumlemF  21058  cpmadumatpoly  21065  cayhamlem3  21069  cayhamlem4  21070  cayleyhamilton0  21071  cayleyhamiltonALT  21073  neiptopnei  21314  neiptopreu  21315  ptcnplem  21802  cnmpt1t  21846  cnmpt12  21848  cnmptkp  21861  cnmptk1  21862  cnmpt1k  21863  cnmptkk  21864  cnmptk1p  21866  cnmpt2k  21869  qtopeu  21897  pt1hmeo  21987  ptunhmeo  21989  xkocnv  21995  xkohmeo  21996  flfcnp2  22188  cnmpt1plusg  22268  istgp2  22272  tmdmulg  22273  tgpmulg  22274  tmdgsum  22276  symgtgp  22282  subgtgp  22286  tgpconncomp  22293  prdstgpd  22305  tsmsmhm  22326  tsmsadd  22327  tsmssub  22329  tgptsmscls  22330  tsmssplit  22332  tsmsxplem1  22333  tsmsxplem2  22334  cnmpt1vsca  22374  tlmtgp  22376  ustuqtoplem  22420  utopsnneip  22429  ressprdsds  22553  metuval  22731  nmfval2  22772  tngnm  22832  nmoeq0  22917  idnghm  22924  cnmpt1ds  23022  fsumcn  23050  expcn  23052  divccn  23053  divccncf  23086  negcncf  23098  copco  23194  pcopt  23198  pcopt2  23199  pcoass  23200  pi1xfrcnvlem  23232  cnmpt1ip  23422  rrxnm  23566  rrxds  23568  minveclem3b  23603  divcncf  23620  ovolctb  23663  ovoliunnul  23680  voliunlem3  23725  ovolfs2  23744  uniioombllem2  23756  vitalilem4  23784  vitalilem5  23785  ismbf  23801  mbfss  23819  mbfmulc2re  23821  mbfneg  23823  mbfpos  23824  mbfposb  23826  mbfadd  23834  mbfsub  23835  mbfmulc2  23836  mbfinf  23838  mbflimsup  23839  mbflimlem  23840  i1fpos  23879  i1fposd  23880  itg1climres  23887  mbfmul  23899  itg2mulc  23920  itg2i1fseq  23928  itg2cnlem1  23934  itg2cnlem2  23935  itgresr  23951  iblneg  23975  i1fibl  23980  itgitg1  23981  iblsub  23994  itgfsum  23999  itgmulc2lem1  24004  limcmpt  24053  limccnp  24061  limcco  24063  dvreslem  24079  dvres2lem  24080  dvidlem  24085  dvcnp2  24089  dvaddbr  24107  dvmulbr  24108  dvmulf  24112  dvcmulf  24114  dvcobr  24115  dvcof  24117  dvcjbr  24118  dvcj  24119  dvfre  24120  dvexp  24122  dvexp2  24123  dvrec  24124  dvmptcmul  24133  dvmptdivc  24134  dvmptneg  24135  dvmptsub  24136  dvmptre  24138  dvmptim  24139  dvrecg  24142  dvmptdiv  24143  dvmptfsum  24144  dvcnvlem  24145  dvcnv  24146  dvexp3  24147  dvef  24149  dvsincos  24150  dv11cn  24170  lhop2  24184  lhop  24185  ftc2  24213  itgparts  24216  itgsubstlem  24217  mdegfval  24228  mdegmullem  24244  ply1termlem  24365  plypow  24367  plyconst  24368  plyeq0lem  24372  plypf1  24374  plyaddlem1  24375  plymullem1  24376  coeeulem  24386  coeidlem  24399  plyco  24403  coeeq2  24404  0dgr  24407  0dgrb  24408  dgrcolem1  24435  dgrcolem2  24436  plycjlem  24438  dvply1  24445  dvply2g  24446  plydiveu  24459  plyremlem  24465  elqaalem3  24482  taylfval  24519  dvtaylp  24530  taylthlem1  24533  taylthlem2  24534  ulmshft  24550  mtestbdd  24565  iblulm  24567  itgulm2  24569  pserulm  24582  psercn2  24583  pserdvlem2  24588  pserdv  24589  pserdv2  24590  abelthlem1  24591  abelthlem3  24593  advlog  24806  advlogexp  24807  dvcxp1  24890  dvcxp2  24891  dvcncxp1  24893  sqrtcn  24900  loglesqrt  24908  dvatan  25082  atantayl2  25085  atantayl3  25086  leibpi  25089  rlimcnp2  25113  efrlim  25116  dfef2  25117  cxp2lim  25123  divsqrtsumlem  25126  lgamgulmlem2  25176  lgamgulm2  25182  lgamcvglem  25186  gamcvg2lem  25205  ftalem7  25225  basellem9  25235  muinv  25339  logfacrlim  25369  logexprlim  25370  dchrmulid2  25397  dchrinvcl  25398  lgseisenlem3  25522  lgseisenlem4  25523  chtppilimlem2  25583  chebbnd2  25586  chpchtlim  25588  chpo1ub  25589  rpvmasumlem  25596  dchrmusumlema  25602  dchrvmasumlem1  25604  dchrvmasumiflem2  25611  dchrisum0fno1  25620  rpvmasum2  25621  dchrisum0lema  25623  dchrisum0lem1  25625  dchrisum0lem2a  25626  dchrisum0lem2  25627  dchrisum0  25629  dchrmusumlem  25631  dchrvmasumlem  25632  rpvmasum  25635  rplogsum  25636  logdivsum  25642  mulog2sumlem3  25645  vmalogdivsum2  25647  vmalogdivsum  25648  2vmadivsumlem  25649  logsqvma2  25652  log2sumbnd  25653  selberglem2  25655  selberg3lem1  25666  selberg3  25668  selberg4lem1  25669  selberg4  25670  pntrsumo1  25674  selberg3r  25678  selberg4r  25679  selberg34r  25680  pntrlog2bndlem2  25687  pntrlog2bndlem4  25689  pntrlog2bndlem5  25690  pntrlog2bndlem6  25692  padicabvf  25740  padicabvcxp  25741  mirval  25974  crctcshlem4  27126  clwlknf1oclwwlkn  27451  clwlknf1oclwwlknOLD  27453  eucrct2eupthOLD  27619  eucrct2eupth  27620  chscllem4  29050  brafnmul  29361  kbmul  29365  ofresid  29989  ofoprabco  30009  fcobijfs  30045  gsummpt2d  30322  gsummptres  30325  fzto1st1  30393  fzto1st  30394  mdetpmtr1  30430  mdetlap  30439  xrge0mulc1cn  30528  esumval  30649  esumsnf  30667  esumpcvgval  30681  esumcvg  30689  esumcvgsum  30691  esumsup  30692  ofcfeqd2  30704  meascnbl  30823  sitgval  30935  probmeasb  31034  cndprobprob  31042  dstfrvclim1  31081  ballotlemfval  31093  ballotlemsval  31112  ballotlemieq  31120  plymul02  31166  plymulx0  31167  plymulx  31168  signsplypnf  31170  signstfv  31183  signstfvn  31189  signstfvp  31192  itgexpif  31229  logdivsqrle  31273  ptpconn  31757  cvmliftlem6  31814  cvmliftphtlem  31841  cvmlift3lem5  31847  elmrsubrn  31959  msubfval  31963  msubco  31970  divcnvlin  32156  knoppcnlem9  33019  knoppcnlem10  33020  knoppcnlem11  33021  bj-finsumval0  33694  curf  33925  matunitlindflem1  33944  matunitlindflem2  33945  poimirlem3  33951  poimirlem15  33963  poimirlem16  33964  poimirlem17  33965  poimirlem19  33967  poimirlem20  33968  broucube  33982  ovoliunnfl  33990  voliunnfl  33992  volsupnfl  33993  mbfposadd  33995  itg2addnclem  33999  itg2addnclem3  34001  itg2addnc  34002  itgaddnclem2  34007  itgaddnc  34008  iblsubnc  34009  itgsubnc  34010  itgmulc2nclem1  34014  itgmulc2nclem2  34015  itgmulc2nc  34016  itgabsnc  34017  ftc1cnnclem  34021  ftc1anclem3  34025  ftc1anclem5  34027  ftc1anclem6  34028  ftc1anclem8  34030  ftc1anc  34031  ftc2nc  34032  areacirclem1  34038  areacirclem2  34039  areacirclem4  34041  areacirc  34043  upixp  34062  mzpsubst  38150  mzprename  38151  mzpcompact2lem  38153  eldioph2  38164  rabdiophlem2  38205  mendlmod  38601  mendassa  38602  areaquad  38639  fsovcnvlem  39142  hashnzfzclim  39356  expgrowthi  39367  expgrowth  39369  uzmptshftfval  39380  dvradcnv2  39381  binomcxplemrat  39384  binomcxplemfrat  39385  binomcxplemradcnv  39386  binomcxplemdvbinom  39387  binomcxplemcvg  39388  binomcxplemdvsum  39389  binomcxplemnotnn0  39390  mulc1cncfg  40610  expcnfg  40612  fprodcnlem  40620  clim1fr1  40622  divcnvg  40648  sublimc  40673  reclimc  40674  divlimc  40677  limsupresico  40721  limsuppnfdlem  40722  limsupvaluz  40729  supcnvlimsupmpt  40762  liminfresico  40792  climliminflimsupd  40822  cncfmptssg  40872  negcncfg  40883  cncficcgt0  40890  fprodcncf  40903  fprodsubrecnncnvlem  40910  fprodaddrecnncnvlem  40912  dvsinax  40916  dvasinbx  40924  dvdivf  40926  ioodvbdlimc1lem2  40936  ioodvbdlimc2lem  40938  dvnmptdivc  40942  dvxpaek  40944  dvnxpaek  40946  dvnmul  40947  dvnprodlem2  40951  ibliccsinexp  40955  itgsinexplem1  40958  itgsinexp  40959  iblempty  40969  itgcoscmulx  40973  itgsincmulx  40978  itgioocnicc  40981  iblcncfioo  40982  itgsbtaddcnst  40986  volioofmpt  40999  volicofmpt  41002  stoweidlem4  41009  stirlinglem5  41083  dirkerval  41096  dirkertrigeq  41106  dirkeritg  41107  dirkercncflem2  41109  dirkercncflem4  41111  fourierdlem16  41128  fourierdlem18  41130  fourierdlem21  41133  fourierdlem22  41134  fourierdlem28  41140  fourierdlem39  41151  fourierdlem40  41152  fourierdlem41  41153  fourierdlem53  41164  fourierdlem56  41167  fourierdlem57  41168  fourierdlem60  41171  fourierdlem61  41172  fourierdlem68  41179  fourierdlem73  41184  fourierdlem74  41185  fourierdlem75  41186  fourierdlem76  41187  fourierdlem78  41189  fourierdlem81  41192  fourierdlem82  41193  fourierdlem83  41194  fourierdlem84  41195  fourierdlem85  41196  fourierdlem88  41199  fourierdlem90  41201  fourierdlem92  41203  fourierdlem93  41204  fourierdlem95  41206  fourierdlem97  41208  fourierdlem101  41212  fourierdlem103  41214  fourierdlem104  41215  fourierdlem111  41222  fourierdlem112  41223  sqwvfoura  41233  sqwvfourb  41234  fouriersw  41236  elaa2lem  41238  etransclem4  41243  etransclem17  41256  etransclem18  41257  etransclem32  41271  etransclem46  41285  sge0z  41377  sge0revalmpt  41380  sge0tsms  41382  sge0sup  41393  sge0iunmptlemre  41417  sge0iun  41421  sge0xaddlem2  41436  ismeannd  41469  psmeasurelem  41472  meaiuninclem  41482  meaiininclem  41488  caratheodory  41530  isomenndlem  41532  ovnval  41543  hoicvrrex  41558  ovnlecvr  41560  ovncvrrp  41566  ovn0lem  41567  ovnsubaddlem1  41572  hoidmv1lelem2  41594  hoidmv1le  41596  hoidmvlelem3  41599  ovnhoilem2  41604  ovnhoi  41605  ovnlecvr2  41612  ovncvr2  41613  hspmbllem2  41629  ovolval2lem  41645  ovolval3  41649  ovolval5lem1  41654  ovolval5lem2  41655  ovnovollem1  41658  ovnovollem2  41659  vonioolem1  41682  vonicclem1  41685  vonct  41695  smflim  41773  smfinflem  41811  smflimsuplem5  41818  smfliminflem  41824  fdmdifeqresdif  42981  ply1mulgsumlem2  43036  lincvalsc0  43071  linc0scn0  43073  lincdifsn  43074  lincsum  43079  lincscm  43080  lindslinindimp2lem4  43111  lindslinindsimp2lem5  43112  lincresunit3lem2  43130  aacllem  43453  amgmwlem  43454