Theorem mpteq2dva 5179

Description: Slightly more general equality inference for the maps-to notation. (Contributed by Scott Fenton, 25-Apr-2012.) Remove dependency on ax-10 2147. (Revised by SN, 11-Nov-2024.)

Hypothesis

Ref	Expression
mpteq2dva.1	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)

Assertion

Ref	Expression
mpteq2dva	⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)   𝐶(𝑥)

Proof of Theorem mpteq2dva

Step	Hyp	Ref	Expression
1		eqidd 2738	. 2 ⊢ (𝜑 → 𝐴 = 𝐴)
2		mpteq2dva.1	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)
3	1, 2	mpteq12dva 5172	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114   ↦ cmpt 5167

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-opab 5149  df-mpt 5168

This theorem is referenced by:  mpteq2dv  5180  mpteq2ia  5181  2fvcoidd  7245  offval  7633  offval2  7644  coof  7648  caofinvl  7656  caofcom  7661  caofass  7664  caofdi  7666  caofdir  7667  caonncan  7668  curry1  8047  curry2  8050  mpocurryd  8212  pw2f1olem  9012  mapxpen  9074  xpmapenlem  9075  cantnfp1  9593  cantnflem1d  9600  cantnflem1  9601  cnfcom2lem  9613  dfac12lem1  10057  seqof  14012  seqof2  14013  swrdswrd  14658  repswswrd  14737  repswrevw  14740  revco  14787  ccatco  14788  repsco  14793  ofccat  14922  lo1eq  15521  rlimeq  15522  lo1mul2  15582  o1dif  15583  lo1sub  15584  rlimdiv  15599  caucvgr  15629  sumeq1  15642  fsumrlim  15765  fsumo1  15766  climfsum  15774  geomulcvg  15832  vdwlem8  16950  prmgapprmo  17024  restid2  17384  pwsplusgval  17445  pwsmulrval  17446  pwsvscafval  17449  qusin  17499  xpsaddlem  17528  xpsvsca  17532  catidd  17637  fuclid  17927  fucrid  17928  fucass  17929  setcepi  18046  prf1st  18161  prf2nd  18162  1st2ndprf  18163  curfcl  18189  curfuncf  18195  diag2  18202  curf2ndf  18204  hof2val  18213  hofcllem  18215  hofcl  18216  yonedalem4a  18232  yonedalem4c  18234  yonedalem3b  18236  yonedainv  18238  yonffthlem  18239  prdssgrpd  18692  prdsidlem  18728  prdsmndd  18729  mhmvlin  18760  pwsco2mhm  18792  frmdup3lem  18825  frmdup3  18826  smndex1gid  18863  smndex1gidOLD  18864  smndex1igidOLD  18866  grpinvpropd  18982  prdsinvlem  19016  pwsinvg  19020  pwssub  19021  galactghm  19370  cayleylem1  19378  pmtrprfval  19453  sylow1lem2  19565  sylow3lem1  19593  efginvrel1  19694  frgpup3lem  19743  frgpup3  19744  prdscmnd  19827  iscyggen  19846  gsumval3  19873  gsumcllem  19874  gsumzsplit  19893  gsumsub  19914  gsummptf1o  19929  gsum2d  19938  gsum2d2  19940  gsumxp  19942  prdsgsum  19947  telgsumfz  19956  telgsumfz0  19958  telgsum  19960  dprdfsub  19989  dprdfeq0  19990  dprddisj2  20007  dprd2d2  20012  dpjidcl  20026  ablfaclem2  20054  ablfac2  20057  prdsmgp  20123  prdsrngd  20148  srgbinomlem3  20200  srgbinomlem4  20201  srgbinomlem  20202  gsumdixp  20289  prdsringd  20291  pwsgprod  20300  prdslmodd  20955  mulgrhm2  21468  frgpcyg  21563  freshmansdream  21564  evpmodpmf1o  21586  phlpropd  21645  frlmphl  21771  uvcresum  21783  frlmup1  21788  asclpropd  21887  psrass1lem  21922  psrlinv  21944  psrass1  21952  psrdi  21953  psrdir  21954  psrass23l  21955  psrcom  21956  psrass23  21957  resspsrmul  21964  mplsubrglem  21992  mplmonmul  22024  mplcoe1  22025  mplcoe5  22028  mplcoe4  22059  evlslem3  22068  evlslem1  22070  evlsvvval  22081  mhpmulcl  22125  psdmplcl  22138  psdadd  22139  psdmul  22142  psdmvr  22145  psrplusgpropd  22209  psropprmul  22211  coe1mul2  22244  coe1tm  22248  coe1tmmul2  22251  coe1tmmul  22252  coe1pwmul  22254  cply1mul  22271  ply1coe  22273  eqcoe1ply1eq  22274  lply1binomsc  22286  evl1gsummon  22340  evls1fpws  22344  rhmcomulmpl  22357  mamures  22372  grpvrinv  22374  mamuass  22377  mamudi  22378  mamudir  22379  mamuvs1  22380  mamuvs2  22381  mpomatmul  22421  mamutpos  22433  madetsumid  22436  dmatmul  22472  scmatscm  22488  1mavmul  22523  mavmulass  22524  mvmumamul1  22529  mulmarep1gsum1  22548  mulmarep1gsum2  22549  mdetleib2  22563  mdetfval1  22565  mdet0pr  22567  mdetdiag  22574  mdetdiagid  22575  mdetrlin  22577  mdetrsca  22578  mdetralt  22583  mdetunilem9  22595  gsummatr01  22634  smadiadetlem1a  22638  smadiadetlem3  22643  smadiadetlem4  22644  cpmatmcllem  22693  mat2pmatmul  22706  decpmatmullem  22746  decpmatmul  22747  pmatcollpw1lem2  22750  pmatcollpw  22756  pmatcollpw3lem  22758  pmatcollpwscmat  22766  idpm2idmp  22776  mp2pm2mplem3  22783  mp2pm2mplem4  22784  mp2pm2mplem5  22785  mp2pm2mp  22786  pm2mpghm  22791  pm2mpmhmlem2  22794  monmat2matmon  22799  pm2mp  22800  chpdmat  22816  chpscmat  22817  chpscmatgsumbin  22819  chpscmatgsummon  22820  chp0mat  22821  chpidmat  22822  chfacfscmulgsum  22835  chfacfpmmulgsum  22839  chfacfpmmulgsum2  22840  cayhamlem1  22841  cpmidgsumm2pm  22844  cpmidpmat  22848  cpmadugsumlemB  22849  cpmadugsumlemC  22850  cpmadugsumlemF  22851  cpmadumatpoly  22858  cayhamlem3  22862  cayhamlem4  22863  cayleyhamilton0  22864  cayleyhamiltonALT  22866  neiptopnei  23107  neiptopreu  23108  ptcnplem  23596  cnmpt1t  23640  cnmpt12  23642  cnmptkp  23655  cnmptk1  23656  cnmpt1k  23657  cnmptkk  23658  cnmptk1p  23660  cnmpt2k  23663  qtopeu  23691  pt1hmeo  23781  ptunhmeo  23783  xkocnv  23789  xkohmeo  23790  flfcnp2  23982  cnmpt1plusg  24062  istgp2  24066  tmdmulg  24067  tgpmulg  24068  tmdgsum  24070  subgtgp  24080  symgtgp  24081  tgpconncomp  24088  prdstgpd  24100  tsmsmhm  24121  tsmsadd  24122  tsmssub  24124  tgptsmscls  24125  tsmssplit  24127  tsmsxplem1  24128  tsmsxplem2  24129  cnmpt1vsca  24169  tlmtgp  24171  ustuqtoplem  24214  utopsnneip  24223  ressprdsds  24346  metuval  24524  nmfval0  24565  tngnm  24626  nmoeq0  24711  idnghm  24718  cnmpt1ds  24818  fsumcn  24847  expcn  24849  divccn  24850  divccncf  24883  negcncf  24899  copco  24995  pcopt  24999  pcopt2  25000  pcoass  25001  pi1xfrcnvlem  25033  cnmpt1ip  25224  rrxnm  25368  rrxds  25370  minveclem3b  25405  divcncf  25424  ovolctb  25467  ovoliunnul  25484  voliunlem3  25529  ovolfs2  25548  uniioombllem2  25560  vitalilem4  25588  vitalilem5  25589  ismbf  25605  mbfss  25623  mbfmulc2re  25625  mbfneg  25627  mbfpos  25628  mbfposb  25630  mbfadd  25638  mbfsub  25639  mbfmulc2  25640  mbfinf  25642  mbflimsup  25643  mbflimlem  25644  i1fpos  25683  i1fposd  25684  itg1climres  25691  mbfmul  25703  itg2mulc  25724  itg2i1fseq  25732  itg2cnlem1  25738  itg2cnlem2  25739  itgresr  25756  iblneg  25780  i1fibl  25785  itgitg1  25786  iblsub  25799  itgfsum  25804  itgmulc2lem1  25809  limcmpt  25860  limccnp  25868  limcco  25870  dvreslem  25886  dvres2lem  25887  dvidlem  25892  dvcnp2  25897  dvaddbr  25915  dvmulbr  25916  dvmulf  25920  dvcmulf  25922  dvcobr  25923  dvcof  25925  dvcjbr  25926  dvcj  25927  dvfre  25928  dvexp  25930  dvexp2  25931  dvrec  25932  dvmptcmul  25941  dvmptdivc  25942  dvmptneg  25943  dvmptsub  25944  dvmptre  25946  dvmptim  25947  dvrecg  25950  dvmptdiv  25951  dvmptfsum  25952  dvcnvlem  25953  dvcnv  25954  dvexp3  25955  dvef  25957  dvsincos  25958  dv11cn  25978  lhop2  25992  lhop  25993  ftc2  26021  itgparts  26024  itgsubstlem  26025  mdegfval  26037  mdegmullem  26053  ply1termlem  26178  plypow  26180  plyconst  26181  plyeq0lem  26185  plypf1  26187  plyaddlem1  26188  plymullem1  26189  coeeulem  26199  coeidlem  26212  plyco  26216  coeeq2  26217  0dgr  26220  0dgrb  26221  dgrcolem1  26248  dgrcolem2  26249  plycjlem  26251  dvply1  26260  dvply2g  26261  dvply2gOLD  26262  plydiveu  26275  plyremlem  26281  elqaalem3  26298  taylfval  26335  dvtaylp  26347  taylthlem1  26350  taylthlem2  26351  taylthlem2OLD  26352  ulmshft  26368  mtestbdd  26383  iblulm  26385  itgulm2  26387  pserulm  26400  psercn2  26401  pserdvlem2  26406  pserdv  26407  pserdv2  26408  abelthlem1  26409  abelthlem3  26411  advlog  26631  advlogexp  26632  dvcxp1  26717  dvcxp2  26718  dvcncxp1  26720  sqrtcn  26727  loglesqrt  26738  dvatan  26912  atantayl2  26915  atantayl3  26916  leibpi  26919  rlimcnp2  26943  efrlim  26946  efrlimOLD  26947  dfef2  26948  cxp2lim  26954  divsqrtsumlem  26957  lgamgulmlem2  27007  lgamgulm2  27013  lgamcvglem  27017  gamcvg2lem  27036  ftalem7  27056  basellem9  27066  muinv  27170  logfacrlim  27201  logexprlim  27202  dchrmullid  27229  dchrinvcl  27230  lgseisenlem3  27354  lgseisenlem4  27355  chtppilimlem2  27451  chebbnd2  27454  chpchtlim  27456  chpo1ub  27457  rpvmasumlem  27464  dchrmusumlema  27470  dchrvmasumlem1  27472  dchrvmasumiflem2  27479  dchrisum0fno1  27488  rpvmasum2  27489  dchrisum0lema  27491  dchrisum0lem1  27493  dchrisum0lem2a  27494  dchrisum0lem2  27495  dchrisum0  27497  dchrmusumlem  27499  dchrvmasumlem  27500  rpvmasum  27503  rplogsum  27504  logdivsum  27510  mulog2sumlem3  27513  vmalogdivsum2  27515  vmalogdivsum  27516  2vmadivsumlem  27517  logsqvma2  27520  log2sumbnd  27521  selberglem2  27523  selberg3lem1  27534  selberg3  27536  selberg4lem1  27537  selberg4  27538  pntrsumo1  27542  selberg3r  27546  selberg4r  27547  selberg34r  27548  pntrlog2bndlem2  27555  pntrlog2bndlem4  27557  pntrlog2bndlem5  27558  pntrlog2bndlem6  27560  padicabvf  27608  padicabvcxp  27609  mirval  28737  crctcshlem4  29903  clwlknf1oclwwlkn  30169  eucrct2eupth  30330  chscllem4  31726  brafnmul  32037  kbmul  32041  cofmpt2  32722  ofresid  32730  ofoprabco  32752  fmptunsnop  32788  fcobijfs  32809  fcobijfs2  32810  gsummpt2d  33125  gsummptres  33128  gsummptres2  33129  gsummptf1od  33131  gsummptp1  33133  gsummptfsf1o  33136  gsumfs2d  33137  gsumpart  33139  gsumhashmul  33143  gsummulsubdishift1  33144  gsummulsubdishift2  33145  gsumwrd2dccat  33154  fzto1st1  33178  fzto1st  33179  elrgspnlem1  33318  elrgspnlem2  33319  elrgspnlem3  33320  elrgspnlem4  33321  elrgspnsubrunlem1  33323  elrgspnsubrunlem2  33324  qusbas2  33481  qusima  33483  elrspunidl  33503  elrspunsn  33504  rprmdvdsprod  33609  ressply1evls1  33640  evl1deg1  33651  evl1deg2  33652  evl1deg3  33653  gsummoncoe1fzo  33672  mplmulmvr  33698  evlextv  33701  mplvrpmga  33704  mplvrpmmhm  33705  mplvrpmrhm  33706  psrgsum  33707  psrmonmul  33709  issply  33720  esplyfval0  33723  esplyfval3  33731  esplyfval1  33732  esplyfvaln  33733  esplyind  33734  vietalem  33738  lbsdiflsp0  33786  fedgmullem1  33789  fedgmullem2  33790  fldextrspunlsplem  33833  fldextrspunlsp  33834  extdgfialglem2  33853  mdetpmtr1  33983  mdetlap  33992  xrge0mulc1cn  34101  esumval  34206  esumsnf  34224  esumpcvgval  34238  esumcvg  34246  esumcvgsum  34248  esumsup  34249  ofcfeqd2  34261  meascnbl  34379  sitgval  34492  probmeasb  34590  cndprobprob  34598  dstfrvclim1  34638  ballotlemfval  34650  ballotlemsval  34669  ballotlemieq  34677  plymul02  34706  plymulx0  34707  plymulx  34708  signsplypnf  34710  signstfv  34723  signstfvn  34729  signstfvp  34731  itgexpif  34766  logdivsqrle  34810  ptpconn  35431  cvmliftlem6  35488  cvmliftphtlem  35515  cvmlift3lem5  35521  elmrsubrn  35718  msubfval  35722  msubco  35729  divcnvlin  35931  knoppcnlem9  36777  knoppcnlem10  36778  knoppcnlem11  36779  bj-finsumval0  37615  curf  37933  matunitlindflem1  37951  matunitlindflem2  37952  poimirlem3  37958  poimirlem15  37970  poimirlem16  37971  poimirlem17  37972  poimirlem19  37974  poimirlem20  37975  broucube  37989  ovoliunnfl  37997  voliunnfl  37999  volsupnfl  38000  mbfposadd  38002  itg2addnclem  38006  itg2addnclem3  38008  itg2addnc  38009  itgaddnclem2  38014  itgaddnc  38015  iblsubnc  38016  itgsubnc  38017  itgmulc2nclem1  38021  itgmulc2nclem2  38022  itgmulc2nc  38023  itgabsnc  38024  ftc1cnnclem  38026  ftc1anclem3  38030  ftc1anclem5  38032  ftc1anclem6  38033  ftc1anclem8  38035  ftc1anc  38036  ftc2nc  38037  areacirclem1  38043  areacirclem2  38044  areacirclem4  38046  areacirc  38048  upixp  38064  lcmineqlem8  42489  lcmineqlem12  42493  dvrelog2b  42519  dvrelogpow2b  42521  aks4d1p1p6  42526  aks4d1p1p5  42528  aks6d1c1  42569  aks6d1c5lem3  42590  sticksstones12a  42610  sticksstones12  42611  sticksstones19  42618  aks6d1c6lem1  42623  aks6d1c6lem4  42626  aks6d1c7lem3  42635  qsalrel  42694  rhmcomulpsr  43008  evlsevl  43021  selvvvval  43032  evlselv  43034  fsuppssindlem1  43038  fsuppssind  43040  mhphf  43044  mzpsubst  43194  mzprename  43195  mzpcompact2lem  43197  eldioph2  43208  rabdiophlem2  43248  mendlmod  43635  mendassa  43636  areaquad  43662  fsovcnvlem  44458  hashnzfzclim  44767  expgrowthi  44778  expgrowth  44780  uzmptshftfval  44791  dvradcnv2  44792  binomcxplemrat  44795  binomcxplemfrat  44796  binomcxplemradcnv  44797  binomcxplemdvbinom  44798  binomcxplemcvg  44799  binomcxplemdvsum  44800  binomcxplemnotnn0  44801  mulc1cncfg  46037  expcnfg  46039  fprodcnlem  46047  clim1fr1  46049  divcnvg  46075  sublimc  46098  reclimc  46099  divlimc  46102  limsupresico  46146  limsuppnfdlem  46147  limsupvaluz  46154  supcnvlimsupmpt  46187  liminfresico  46217  climliminflimsupd  46247  cncfmptssg  46317  negcncfg  46327  cncficcgt0  46334  fprodcncf  46346  fprodsubrecnncnvlem  46353  fprodaddrecnncnvlem  46355  dvsinax  46359  dvasinbx  46366  dvdivf  46368  ioodvbdlimc1lem2  46378  ioodvbdlimc2lem  46380  dvnmptdivc  46384  dvxpaek  46386  dvnxpaek  46388  dvnmul  46389  dvnprodlem2  46393  ibliccsinexp  46397  itgsinexplem1  46400  itgsinexp  46401  iblempty  46411  itgcoscmulx  46415  itgsincmulx  46420  itgioocnicc  46423  iblcncfioo  46424  itgsbtaddcnst  46428  volioofmpt  46440  volicofmpt  46443  stoweidlem4  46450  stirlinglem5  46524  dirkerval  46537  dirkertrigeq  46547  dirkeritg  46548  dirkercncflem2  46550  dirkercncflem4  46552  fourierdlem16  46569  fourierdlem18  46571  fourierdlem21  46574  fourierdlem22  46575  fourierdlem28  46581  fourierdlem39  46592  fourierdlem40  46593  fourierdlem41  46594  fourierdlem53  46605  fourierdlem56  46608  fourierdlem57  46609  fourierdlem60  46612  fourierdlem61  46613  fourierdlem68  46620  fourierdlem73  46625  fourierdlem74  46626  fourierdlem75  46627  fourierdlem76  46628  fourierdlem78  46630  fourierdlem81  46633  fourierdlem82  46634  fourierdlem83  46635  fourierdlem84  46636  fourierdlem85  46637  fourierdlem88  46640  fourierdlem90  46642  fourierdlem92  46644  fourierdlem93  46645  fourierdlem95  46647  fourierdlem97  46649  fourierdlem101  46653  fourierdlem103  46655  fourierdlem104  46656  fourierdlem111  46663  fourierdlem112  46664  sqwvfoura  46674  sqwvfourb  46675  fouriersw  46677  elaa2lem  46679  etransclem4  46684  etransclem17  46697  etransclem18  46698  etransclem32  46712  etransclem46  46726  sge0z  46821  sge0revalmpt  46824  sge0tsms  46826  sge0sup  46837  sge0iunmptlemre  46861  sge0iun  46865  sge0xaddlem2  46880  ismeannd  46913  psmeasurelem  46916  meaiuninclem  46926  meaiininclem  46932  caratheodory  46974  isomenndlem  46976  ovnval  46987  hoicvrrex  47002  ovnlecvr  47004  ovncvrrp  47010  ovn0lem  47011  ovnsubaddlem1  47016  hoidmv1lelem2  47038  hoidmv1le  47040  hoidmvlelem3  47043  ovnhoilem2  47048  ovnhoi  47049  ovnlecvr2  47056  ovncvr2  47057  hspmbllem2  47073  ovolval2lem  47089  ovolval3  47093  ovolval5lem1  47098  ovolval5lem2  47099  ovnovollem1  47102  ovnovollem2  47103  vonioolem1  47126  vonicclem1  47129  vonct  47139  smflim  47223  smfinflem  47263  smflimsuplem5  47270  smfliminflem  47276  cfsetsnfsetfv  47517  fundcmpsurbijinjpreimafv  47879  fundcmpsurinjimaid  47883  fdmdifeqresdif  48830  ply1mulgsumlem2  48875  lincvalsc0  48909  linc0scn0  48911  lincdifsn  48912  lincsum  48917  lincscm  48918  lindslinindimp2lem4  48949  lindslinindsimp2lem5  48950  lincresunit3lem2  48968  1arymaptfo  49131  itcovalpclem1  49158  itcovalpclem2  49159  itcovalt2lem1  49163  itcovalt2lem2  49164  tposcurf1  49786  tposcurf2  49787  diag1  49791  fuco22  49826  fucocolem2  49841  fucocolem3  49842  fucocolem4  49843  fucoco  49844  fucolid  49848  fucorid  49849  postcofval  49851  precofval  49854  precofvalALT  49855  precofval2  49856  fucoppcco  49896  islmd  50152  iscmd  50153  aacllem  50288  amgmwlem  50289