Theorem mpteq2dva 5164

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 1914	. 2 ⊢ Ⅎ𝑥𝜑
2		mpteq2dva.1	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)
3	1, 2	mpteq2da 5163	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1536   ∈ wcel 2113   ↦ cmpt 5149

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-12 2176  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-ral 3146  df-opab 5132  df-mpt 5150

This theorem is referenced by:  mpteq2dv  5165  2fvcoidd  7056  offval  7419  offval2  7429  caofinvl  7439  caofcom  7444  caofass  7446  caofdi  7448  caofdir  7449  caonncan  7450  curry1  7802  curry2  7805  mpocurryd  7938  pw2f1olem  8624  mapxpen  8686  xpmapenlem  8687  cantnfp1  9147  cantnflem1d  9154  cantnflem1  9155  cnfcom2lem  9167  dfac12lem1  9572  seqof  13430  seqof2  13431  swrdswrd  14070  repswswrd  14149  repswrevw  14152  revco  14199  ccatco  14200  repsco  14205  ofccat  14332  lo1eq  14928  rlimeq  14929  lo1mul2  14988  o1dif  14989  lo1sub  14990  rlimdiv  15005  caucvgr  15035  sumeq1  15048  fsumrlim  15169  fsumo1  15170  climfsum  15178  geomulcvg  15235  vdwlem8  16327  prmgapprmo  16401  restid2  16707  pwsplusgval  16766  pwsmulrval  16767  pwsvscafval  16770  qusin  16820  xpsaddlem  16849  xpsvsca  16853  catidd  16954  fuclid  17239  fucrid  17240  fucass  17241  setcepi  17351  prf1st  17457  prf2nd  17458  1st2ndprf  17459  curfcl  17485  curfuncf  17491  diag2  17498  curf2ndf  17500  hof2val  17509  hofcllem  17511  hofcl  17512  yonedalem4a  17528  yonedalem4c  17530  yonedalem3b  17532  yonedainv  17534  yonffthlem  17535  prdsidlem  17946  prdsmndd  17947  pwsco2mhm  18000  frmdup3lem  18034  frmdup3  18035  smndex1gid  18071  smndex1igid  18072  grpinvpropd  18177  prdsinvlem  18211  pwsinvg  18215  pwssub  18216  galactghm  18535  cayleylem1  18543  pmtrprfval  18618  sylow1lem2  18727  sylow3lem1  18755  efginvrel1  18857  frgpup3lem  18906  frgpup3  18907  prdscmnd  18984  iscyggen  19002  gsumval3  19030  gsumcllem  19031  gsumzsplit  19050  gsumsub  19071  gsummptf1o  19086  gsum2d  19095  gsum2d2  19097  gsumxp  19099  prdsgsum  19104  telgsumfz  19113  telgsumfz0  19115  telgsum  19117  dprdfsub  19146  dprdfeq0  19147  dprddisj2  19164  dprd2d2  19169  dpjidcl  19183  ablfaclem2  19211  ablfac2  19214  srgbinomlem3  19295  srgbinomlem4  19296  srgbinomlem  19297  gsumdixp  19362  prdsmgp  19363  prdsringd  19365  prdslmodd  19744  asclpropd  20129  psrass1lem  20160  psrlinv  20180  psrass1  20188  psrdi  20189  psrdir  20190  psrass23l  20191  psrcom  20192  psrass23  20193  resspsrmul  20200  mplsubrglem  20222  mplmonmul  20248  mplcoe1  20249  mplcoe5  20252  mplcoe4  20286  evlslem3  20296  evlslem1  20298  psrplusgpropd  20407  psropprmul  20409  coe1mul2  20440  coe1tm  20444  coe1tmmul2  20447  coe1tmmul  20448  coe1pwmul  20450  cply1mul  20465  ply1coe  20467  eqcoe1ply1eq  20468  lply1binomsc  20478  evl1gsummon  20531  mulgrhm2  20649  frgpcyg  20723  evpmodpmf1o  20743  phlpropd  20802  frlmphl  20928  uvcresum  20940  frlmup1  20945  mamures  21004  grpvrinv  21010  mhmvlin  21011  mamuass  21014  mamudi  21015  mamudir  21016  mamuvs1  21017  mamuvs2  21018  mpomatmul  21058  mamutpos  21070  madetsumid  21073  dmatmul  21109  scmatscm  21125  1mavmul  21160  mavmulass  21161  mvmumamul1  21166  mulmarep1gsum1  21185  mulmarep1gsum2  21186  mdetleib2  21200  mdetfval1  21202  mdet0pr  21204  mdetdiag  21211  mdetdiagid  21212  mdetrlin  21214  mdetrsca  21215  mdetralt  21220  mdetunilem9  21232  gsummatr01  21271  smadiadetlem1a  21275  smadiadetlem3  21280  smadiadetlem4  21281  cpmatmcllem  21329  mat2pmatmul  21342  decpmatmullem  21382  decpmatmul  21383  pmatcollpw1lem2  21386  pmatcollpw  21392  pmatcollpw3lem  21394  pmatcollpwscmat  21402  idpm2idmp  21412  mp2pm2mplem3  21419  mp2pm2mplem4  21420  mp2pm2mplem5  21421  mp2pm2mp  21422  pm2mpghm  21427  pm2mpmhmlem2  21430  monmat2matmon  21435  pm2mp  21436  chpdmat  21452  chpscmat  21453  chpscmatgsumbin  21455  chpscmatgsummon  21456  chp0mat  21457  chpidmat  21458  chfacfscmulgsum  21471  chfacfpmmulgsum  21475  chfacfpmmulgsum2  21476  cayhamlem1  21477  cpmidgsumm2pm  21480  cpmidpmat  21484  cpmadugsumlemB  21485  cpmadugsumlemC  21486  cpmadugsumlemF  21487  cpmadumatpoly  21494  cayhamlem3  21498  cayhamlem4  21499  cayleyhamilton0  21500  cayleyhamiltonALT  21502  neiptopnei  21743  neiptopreu  21744  ptcnplem  22232  cnmpt1t  22276  cnmpt12  22278  cnmptkp  22291  cnmptk1  22292  cnmpt1k  22293  cnmptkk  22294  cnmptk1p  22296  cnmpt2k  22299  qtopeu  22327  pt1hmeo  22417  ptunhmeo  22419  xkocnv  22425  xkohmeo  22426  flfcnp2  22618  cnmpt1plusg  22698  istgp2  22702  tmdmulg  22703  tgpmulg  22704  tmdgsum  22706  subgtgp  22716  symgtgp  22717  tgpconncomp  22724  prdstgpd  22736  tsmsmhm  22757  tsmsadd  22758  tsmssub  22760  tgptsmscls  22761  tsmssplit  22763  tsmsxplem1  22764  tsmsxplem2  22765  cnmpt1vsca  22805  tlmtgp  22807  ustuqtoplem  22851  utopsnneip  22860  ressprdsds  22984  metuval  23162  nmfval2  23203  tngnm  23263  nmoeq0  23348  idnghm  23355  cnmpt1ds  23453  fsumcn  23481  expcn  23483  divccn  23484  divccncf  23517  negcncf  23529  copco  23625  pcopt  23629  pcopt2  23630  pcoass  23631  pi1xfrcnvlem  23663  cnmpt1ip  23853  rrxnm  23997  rrxds  23999  minveclem3b  24034  divcncf  24051  ovolctb  24094  ovoliunnul  24111  voliunlem3  24156  ovolfs2  24175  uniioombllem2  24187  vitalilem4  24215  vitalilem5  24216  ismbf  24232  mbfss  24250  mbfmulc2re  24252  mbfneg  24254  mbfpos  24255  mbfposb  24257  mbfadd  24265  mbfsub  24266  mbfmulc2  24267  mbfinf  24269  mbflimsup  24270  mbflimlem  24271  i1fpos  24310  i1fposd  24311  itg1climres  24318  mbfmul  24330  itg2mulc  24351  itg2i1fseq  24359  itg2cnlem1  24365  itg2cnlem2  24366  itgresr  24382  iblneg  24406  i1fibl  24411  itgitg1  24412  iblsub  24425  itgfsum  24430  itgmulc2lem1  24435  limcmpt  24484  limccnp  24492  limcco  24494  dvreslem  24510  dvres2lem  24511  dvidlem  24516  dvcnp2  24520  dvaddbr  24538  dvmulbr  24539  dvmulf  24543  dvcmulf  24545  dvcobr  24546  dvcof  24548  dvcjbr  24549  dvcj  24550  dvfre  24551  dvexp  24553  dvexp2  24554  dvrec  24555  dvmptcmul  24564  dvmptdivc  24565  dvmptneg  24566  dvmptsub  24567  dvmptre  24569  dvmptim  24570  dvrecg  24573  dvmptdiv  24574  dvmptfsum  24575  dvcnvlem  24576  dvcnv  24577  dvexp3  24578  dvef  24580  dvsincos  24581  dv11cn  24601  lhop2  24615  lhop  24616  ftc2  24644  itgparts  24647  itgsubstlem  24648  mdegfval  24659  mdegmullem  24675  ply1termlem  24796  plypow  24798  plyconst  24799  plyeq0lem  24803  plypf1  24805  plyaddlem1  24806  plymullem1  24807  coeeulem  24817  coeidlem  24830  plyco  24834  coeeq2  24835  0dgr  24838  0dgrb  24839  dgrcolem1  24866  dgrcolem2  24867  plycjlem  24869  dvply1  24876  dvply2g  24877  plydiveu  24890  plyremlem  24896  elqaalem3  24913  taylfval  24950  dvtaylp  24961  taylthlem1  24964  taylthlem2  24965  ulmshft  24981  mtestbdd  24996  iblulm  24998  itgulm2  25000  pserulm  25013  psercn2  25014  pserdvlem2  25019  pserdv  25020  pserdv2  25021  abelthlem1  25022  abelthlem3  25024  advlog  25240  advlogexp  25241  dvcxp1  25324  dvcxp2  25325  dvcncxp1  25327  sqrtcn  25334  loglesqrt  25342  dvatan  25516  atantayl2  25519  atantayl3  25520  leibpi  25523  rlimcnp2  25547  efrlim  25550  dfef2  25551  cxp2lim  25557  divsqrtsumlem  25560  lgamgulmlem2  25610  lgamgulm2  25616  lgamcvglem  25620  gamcvg2lem  25639  ftalem7  25659  basellem9  25669  muinv  25773  logfacrlim  25803  logexprlim  25804  dchrmulid2  25831  dchrinvcl  25832  lgseisenlem3  25956  lgseisenlem4  25957  chtppilimlem2  26053  chebbnd2  26056  chpchtlim  26058  chpo1ub  26059  rpvmasumlem  26066  dchrmusumlema  26072  dchrvmasumlem1  26074  dchrvmasumiflem2  26081  dchrisum0fno1  26090  rpvmasum2  26091  dchrisum0lema  26093  dchrisum0lem1  26095  dchrisum0lem2a  26096  dchrisum0lem2  26097  dchrisum0  26099  dchrmusumlem  26101  dchrvmasumlem  26102  rpvmasum  26105  rplogsum  26106  logdivsum  26112  mulog2sumlem3  26115  vmalogdivsum2  26117  vmalogdivsum  26118  2vmadivsumlem  26119  logsqvma2  26122  log2sumbnd  26123  selberglem2  26125  selberg3lem1  26136  selberg3  26138  selberg4lem1  26139  selberg4  26140  pntrsumo1  26144  selberg3r  26148  selberg4r  26149  selberg34r  26150  pntrlog2bndlem2  26157  pntrlog2bndlem4  26159  pntrlog2bndlem5  26160  pntrlog2bndlem6  26162  padicabvf  26210  padicabvcxp  26211  mirval  26444  crctcshlem4  27601  clwlknf1oclwwlkn  27866  eucrct2eupth  28027  chscllem4  29420  brafnmul  29731  kbmul  29735  cofmpt2  30382  ofresid  30392  ofoprabco  30412  fcobijfs  30462  gsummpt2d  30691  gsummptres  30694  fzto1st1  30748  fzto1st  30749  freshmansdream  30863  lbsdiflsp0  31026  fedgmullem1  31029  fedgmullem2  31030  mdetpmtr1  31092  mdetlap  31101  xrge0mulc1cn  31188  esumval  31309  esumsnf  31327  esumpcvgval  31341  esumcvg  31349  esumcvgsum  31351  esumsup  31352  ofcfeqd2  31364  meascnbl  31482  sitgval  31594  probmeasb  31692  cndprobprob  31700  dstfrvclim1  31739  ballotlemfval  31751  ballotlemsval  31770  ballotlemieq  31778  plymul02  31820  plymulx0  31821  plymulx  31822  signsplypnf  31824  signstfv  31837  signstfvn  31843  signstfvp  31845  itgexpif  31881  logdivsqrle  31925  ptpconn  32484  cvmliftlem6  32541  cvmliftphtlem  32568  cvmlift3lem5  32574  elmrsubrn  32771  msubfval  32775  msubco  32782  divcnvlin  32968  knoppcnlem9  33844  knoppcnlem10  33845  knoppcnlem11  33846  bj-finsumval0  34571  curf  34874  matunitlindflem1  34892  matunitlindflem2  34893  poimirlem3  34899  poimirlem15  34911  poimirlem16  34912  poimirlem17  34913  poimirlem19  34915  poimirlem20  34916  broucube  34930  ovoliunnfl  34938  voliunnfl  34940  volsupnfl  34941  mbfposadd  34943  itg2addnclem  34947  itg2addnclem3  34949  itg2addnc  34950  itgaddnclem2  34955  itgaddnc  34956  iblsubnc  34957  itgsubnc  34958  itgmulc2nclem1  34962  itgmulc2nclem2  34963  itgmulc2nc  34964  itgabsnc  34965  ftc1cnnclem  34969  ftc1anclem3  34973  ftc1anclem5  34975  ftc1anclem6  34976  ftc1anclem8  34978  ftc1anc  34979  ftc2nc  34980  areacirclem1  34986  areacirclem2  34987  areacirclem4  34989  areacirc  34991  upixp  35008  qsalrel  39131  mzpsubst  39351  mzprename  39352  mzpcompact2lem  39354  eldioph2  39365  rabdiophlem2  39405  mendlmod  39799  mendassa  39800  areaquad  39829  fsovcnvlem  40365  hashnzfzclim  40660  expgrowthi  40671  expgrowth  40673  uzmptshftfval  40684  dvradcnv2  40685  binomcxplemrat  40688  binomcxplemfrat  40689  binomcxplemradcnv  40690  binomcxplemdvbinom  40691  binomcxplemcvg  40692  binomcxplemdvsum  40693  binomcxplemnotnn0  40694  mulc1cncfg  41876  expcnfg  41878  fprodcnlem  41886  clim1fr1  41888  divcnvg  41914  sublimc  41939  reclimc  41940  divlimc  41943  limsupresico  41987  limsuppnfdlem  41988  limsupvaluz  41995  supcnvlimsupmpt  42028  liminfresico  42058  climliminflimsupd  42088  cncfmptssg  42159  negcncfg  42170  cncficcgt0  42177  fprodcncf  42190  fprodsubrecnncnvlem  42197  fprodaddrecnncnvlem  42199  dvsinax  42203  dvasinbx  42211  dvdivf  42213  ioodvbdlimc1lem2  42223  ioodvbdlimc2lem  42225  dvnmptdivc  42229  dvxpaek  42231  dvnxpaek  42233  dvnmul  42234  dvnprodlem2  42238  ibliccsinexp  42242  itgsinexplem1  42245  itgsinexp  42246  iblempty  42256  itgcoscmulx  42260  itgsincmulx  42265  itgioocnicc  42268  iblcncfioo  42269  itgsbtaddcnst  42273  volioofmpt  42286  volicofmpt  42289  stoweidlem4  42296  stirlinglem5  42370  dirkerval  42383  dirkertrigeq  42393  dirkeritg  42394  dirkercncflem2  42396  dirkercncflem4  42398  fourierdlem16  42415  fourierdlem18  42417  fourierdlem21  42420  fourierdlem22  42421  fourierdlem28  42427  fourierdlem39  42438  fourierdlem40  42439  fourierdlem41  42440  fourierdlem53  42451  fourierdlem56  42454  fourierdlem57  42455  fourierdlem60  42458  fourierdlem61  42459  fourierdlem68  42466  fourierdlem73  42471  fourierdlem74  42472  fourierdlem75  42473  fourierdlem76  42474  fourierdlem78  42476  fourierdlem81  42479  fourierdlem82  42480  fourierdlem83  42481  fourierdlem84  42482  fourierdlem85  42483  fourierdlem88  42486  fourierdlem90  42488  fourierdlem92  42490  fourierdlem93  42491  fourierdlem95  42493  fourierdlem97  42495  fourierdlem101  42499  fourierdlem103  42501  fourierdlem104  42502  fourierdlem111  42509  fourierdlem112  42510  sqwvfoura  42520  sqwvfourb  42521  fouriersw  42523  elaa2lem  42525  etransclem4  42530  etransclem17  42543  etransclem18  42544  etransclem32  42558  etransclem46  42572  sge0z  42664  sge0revalmpt  42667  sge0tsms  42669  sge0sup  42680  sge0iunmptlemre  42704  sge0iun  42708  sge0xaddlem2  42723  ismeannd  42756  psmeasurelem  42759  meaiuninclem  42769  meaiininclem  42775  caratheodory  42817  isomenndlem  42819  ovnval  42830  hoicvrrex  42845  ovnlecvr  42847  ovncvrrp  42853  ovn0lem  42854  ovnsubaddlem1  42859  hoidmv1lelem2  42881  hoidmv1le  42883  hoidmvlelem3  42886  ovnhoilem2  42891  ovnhoi  42892  ovnlecvr2  42899  ovncvr2  42900  hspmbllem2  42916  ovolval2lem  42932  ovolval3  42936  ovolval5lem1  42941  ovolval5lem2  42942  ovnovollem1  42945  ovnovollem2  42946  vonioolem1  42969  vonicclem1  42972  vonct  42982  smflim  43060  smfinflem  43098  smflimsuplem5  43105  smfliminflem  43111  fundcmpsurbijinjpreimafv  43574  fundcmpsurinjimaid  43578  fdmdifeqresdif  44397  ply1mulgsumlem2  44448  lincvalsc0  44483  linc0scn0  44485  lincdifsn  44486  lincsum  44491  lincscm  44492  lindslinindimp2lem4  44523  lindslinindsimp2lem5  44524  lincresunit3lem2  44542  aacllem  44909  amgmwlem  44910