Theorem mpteq2dva 5247

Description: Slightly more general equality inference for the maps-to notation. (Contributed by Scott Fenton, 25-Apr-2012.) Remove dependency on ax-10 2137. (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 2733	. 2 ⊢ (𝜑 → 𝐴 = 𝐴)
2		mpteq2dva.1	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)
3	1, 2	mpteq12dva 5236	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106   ↦ cmpt 5230

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-opab 5210  df-mpt 5231

This theorem is referenced by:  mpteq2dv  5249  mpteq2ia  5250  2fvcoidd  7291  offval  7675  offval2  7686  caofinvl  7696  caofcom  7701  caofass  7703  caofdi  7705  caofdir  7706  caonncan  7707  curry1  8086  curry2  8089  mpocurryd  8250  pw2f1olem  9072  mapxpen  9139  xpmapenlem  9140  cantnfp1  9672  cantnflem1d  9679  cantnflem1  9680  cnfcom2lem  9692  dfac12lem1  10134  seqof  14021  seqof2  14022  swrdswrd  14651  repswswrd  14730  repswrevw  14733  revco  14781  ccatco  14782  repsco  14787  ofccat  14912  lo1eq  15508  rlimeq  15509  lo1mul2  15569  o1dif  15570  lo1sub  15571  rlimdiv  15588  caucvgr  15618  sumeq1  15631  fsumrlim  15753  fsumo1  15754  climfsum  15762  geomulcvg  15818  vdwlem8  16917  prmgapprmo  16991  restid2  17372  pwsplusgval  17432  pwsmulrval  17433  pwsvscafval  17436  qusin  17486  xpsaddlem  17515  xpsvsca  17519  catidd  17620  fuclid  17915  fucrid  17916  fucass  17917  setcepi  18034  prf1st  18152  prf2nd  18153  1st2ndprf  18154  curfcl  18181  curfuncf  18187  diag2  18194  curf2ndf  18196  hof2val  18205  hofcllem  18207  hofcl  18208  yonedalem4a  18224  yonedalem4c  18226  yonedalem3b  18228  yonedainv  18230  yonffthlem  18231  prdssgrpd  18620  prdsidlem  18653  prdsmndd  18654  pwsco2mhm  18710  frmdup3lem  18743  frmdup3  18744  smndex1gid  18780  smndex1igid  18781  grpinvpropd  18894  prdsinvlem  18928  pwsinvg  18932  pwssub  18933  galactghm  19266  cayleylem1  19274  pmtrprfval  19349  sylow1lem2  19461  sylow3lem1  19489  efginvrel1  19590  frgpup3lem  19639  frgpup3  19640  prdscmnd  19723  iscyggen  19742  gsumval3  19769  gsumcllem  19770  gsumzsplit  19789  gsumsub  19810  gsummptf1o  19825  gsum2d  19834  gsum2d2  19836  gsumxp  19838  prdsgsum  19843  telgsumfz  19852  telgsumfz0  19854  telgsum  19856  dprdfsub  19885  dprdfeq0  19886  dprddisj2  19903  dprd2d2  19908  dpjidcl  19922  ablfaclem2  19950  ablfac2  19953  srgbinomlem3  20044  srgbinomlem4  20045  srgbinomlem  20046  gsumdixp  20124  prdsmgp  20125  prdsringd  20127  prdslmodd  20572  mulgrhm2  21039  frgpcyg  21120  evpmodpmf1o  21140  phlpropd  21199  frlmphl  21327  uvcresum  21339  frlmup1  21344  asclpropd  21442  psrass1lemOLD  21484  psrass1lem  21487  psrlinv  21507  psrass1  21516  psrdi  21517  psrdir  21518  psrass23l  21519  psrcom  21520  psrass23  21521  resspsrmul  21528  mplsubrglem  21554  mplmonmul  21582  mplcoe1  21583  mplcoe5  21586  mplcoe4  21623  evlslem3  21634  evlslem1  21636  mhpmulcl  21683  psrplusgpropd  21749  psropprmul  21751  coe1mul2  21782  coe1tm  21786  coe1tmmul2  21789  coe1tmmul  21790  coe1pwmul  21792  cply1mul  21809  ply1coe  21811  eqcoe1ply1eq  21812  lply1binomsc  21822  evl1gsummon  21875  mamures  21883  grpvrinv  21889  mhmvlin  21890  mamuass  21893  mamudi  21894  mamudir  21895  mamuvs1  21896  mamuvs2  21897  mpomatmul  21939  mamutpos  21951  madetsumid  21954  dmatmul  21990  scmatscm  22006  1mavmul  22041  mavmulass  22042  mvmumamul1  22047  mulmarep1gsum1  22066  mulmarep1gsum2  22067  mdetleib2  22081  mdetfval1  22083  mdet0pr  22085  mdetdiag  22092  mdetdiagid  22093  mdetrlin  22095  mdetrsca  22096  mdetralt  22101  mdetunilem9  22113  gsummatr01  22152  smadiadetlem1a  22156  smadiadetlem3  22161  smadiadetlem4  22162  cpmatmcllem  22211  mat2pmatmul  22224  decpmatmullem  22264  decpmatmul  22265  pmatcollpw1lem2  22268  pmatcollpw  22274  pmatcollpw3lem  22276  pmatcollpwscmat  22284  idpm2idmp  22294  mp2pm2mplem3  22301  mp2pm2mplem4  22302  mp2pm2mplem5  22303  mp2pm2mp  22304  pm2mpghm  22309  pm2mpmhmlem2  22312  monmat2matmon  22317  pm2mp  22318  chpdmat  22334  chpscmat  22335  chpscmatgsumbin  22337  chpscmatgsummon  22338  chp0mat  22339  chpidmat  22340  chfacfscmulgsum  22353  chfacfpmmulgsum  22357  chfacfpmmulgsum2  22358  cayhamlem1  22359  cpmidgsumm2pm  22362  cpmidpmat  22366  cpmadugsumlemB  22367  cpmadugsumlemC  22368  cpmadugsumlemF  22369  cpmadumatpoly  22376  cayhamlem3  22380  cayhamlem4  22381  cayleyhamilton0  22382  cayleyhamiltonALT  22384  neiptopnei  22627  neiptopreu  22628  ptcnplem  23116  cnmpt1t  23160  cnmpt12  23162  cnmptkp  23175  cnmptk1  23176  cnmpt1k  23177  cnmptkk  23178  cnmptk1p  23180  cnmpt2k  23183  qtopeu  23211  pt1hmeo  23301  ptunhmeo  23303  xkocnv  23309  xkohmeo  23310  flfcnp2  23502  cnmpt1plusg  23582  istgp2  23586  tmdmulg  23587  tgpmulg  23588  tmdgsum  23590  subgtgp  23600  symgtgp  23601  tgpconncomp  23608  prdstgpd  23620  tsmsmhm  23641  tsmsadd  23642  tsmssub  23644  tgptsmscls  23645  tsmssplit  23647  tsmsxplem1  23648  tsmsxplem2  23649  cnmpt1vsca  23689  tlmtgp  23691  ustuqtoplem  23735  utopsnneip  23744  ressprdsds  23868  metuval  24049  nmfval0  24090  tngnm  24159  nmoeq0  24244  idnghm  24251  cnmpt1ds  24349  fsumcn  24377  expcn  24379  divccn  24380  divccncf  24413  negcncf  24429  copco  24525  pcopt  24529  pcopt2  24530  pcoass  24531  pi1xfrcnvlem  24563  cnmpt1ip  24755  rrxnm  24899  rrxds  24901  minveclem3b  24936  divcncf  24955  ovolctb  24998  ovoliunnul  25015  voliunlem3  25060  ovolfs2  25079  uniioombllem2  25091  vitalilem4  25119  vitalilem5  25120  ismbf  25136  mbfss  25154  mbfmulc2re  25156  mbfneg  25158  mbfpos  25159  mbfposb  25161  mbfadd  25169  mbfsub  25170  mbfmulc2  25171  mbfinf  25173  mbflimsup  25174  mbflimlem  25175  i1fpos  25215  i1fposd  25216  itg1climres  25223  mbfmul  25235  itg2mulc  25256  itg2i1fseq  25264  itg2cnlem1  25270  itg2cnlem2  25271  itgresr  25287  iblneg  25311  i1fibl  25316  itgitg1  25317  iblsub  25330  itgfsum  25335  itgmulc2lem1  25340  limcmpt  25391  limccnp  25399  limcco  25401  dvreslem  25417  dvres2lem  25418  dvidlem  25423  dvcnp2  25428  dvaddbr  25446  dvmulbr  25447  dvmulf  25451  dvcmulf  25453  dvcobr  25454  dvcof  25456  dvcjbr  25457  dvcj  25458  dvfre  25459  dvexp  25461  dvexp2  25462  dvrec  25463  dvmptcmul  25472  dvmptdivc  25473  dvmptneg  25474  dvmptsub  25475  dvmptre  25477  dvmptim  25478  dvrecg  25481  dvmptdiv  25482  dvmptfsum  25483  dvcnvlem  25484  dvcnv  25485  dvexp3  25486  dvef  25488  dvsincos  25489  dv11cn  25509  lhop2  25523  lhop  25524  ftc2  25552  itgparts  25555  itgsubstlem  25556  mdegfval  25571  mdegmullem  25587  ply1termlem  25708  plypow  25710  plyconst  25711  plyeq0lem  25715  plypf1  25717  plyaddlem1  25718  plymullem1  25719  coeeulem  25729  coeidlem  25742  plyco  25746  coeeq2  25747  0dgr  25750  0dgrb  25751  dgrcolem1  25778  dgrcolem2  25779  plycjlem  25781  dvply1  25788  dvply2g  25789  plydiveu  25802  plyremlem  25808  elqaalem3  25825  taylfval  25862  dvtaylp  25873  taylthlem1  25876  taylthlem2  25877  ulmshft  25893  mtestbdd  25908  iblulm  25910  itgulm2  25912  pserulm  25925  psercn2  25926  pserdvlem2  25931  pserdv  25932  pserdv2  25933  abelthlem1  25934  abelthlem3  25936  advlog  26153  advlogexp  26154  dvcxp1  26237  dvcxp2  26238  dvcncxp1  26240  sqrtcn  26247  loglesqrt  26255  dvatan  26429  atantayl2  26432  atantayl3  26433  leibpi  26436  rlimcnp2  26460  efrlim  26463  dfef2  26464  cxp2lim  26470  divsqrtsumlem  26473  lgamgulmlem2  26523  lgamgulm2  26529  lgamcvglem  26533  gamcvg2lem  26552  ftalem7  26572  basellem9  26582  muinv  26686  logfacrlim  26716  logexprlim  26717  dchrmullid  26744  dchrinvcl  26745  lgseisenlem3  26869  lgseisenlem4  26870  chtppilimlem2  26966  chebbnd2  26969  chpchtlim  26971  chpo1ub  26972  rpvmasumlem  26979  dchrmusumlema  26985  dchrvmasumlem1  26987  dchrvmasumiflem2  26994  dchrisum0fno1  27003  rpvmasum2  27004  dchrisum0lema  27006  dchrisum0lem1  27008  dchrisum0lem2a  27009  dchrisum0lem2  27010  dchrisum0  27012  dchrmusumlem  27014  dchrvmasumlem  27015  rpvmasum  27018  rplogsum  27019  logdivsum  27025  mulog2sumlem3  27028  vmalogdivsum2  27030  vmalogdivsum  27031  2vmadivsumlem  27032  logsqvma2  27035  log2sumbnd  27036  selberglem2  27038  selberg3lem1  27049  selberg3  27051  selberg4lem1  27052  selberg4  27053  pntrsumo1  27057  selberg3r  27061  selberg4r  27062  selberg34r  27063  pntrlog2bndlem2  27070  pntrlog2bndlem4  27072  pntrlog2bndlem5  27073  pntrlog2bndlem6  27075  padicabvf  27123  padicabvcxp  27124  mirval  27895  crctcshlem4  29063  clwlknf1oclwwlkn  29326  eucrct2eupth  29487  chscllem4  30880  brafnmul  31191  kbmul  31195  cofmpt2  31845  ofresid  31854  ofoprabco  31876  fcobijfs  31935  gsummpt2d  32188  gsummptres  32191  gsummptres2  32192  gsumpart  32194  gsumhashmul  32195  fzto1st1  32248  fzto1st  32249  freshmansdream  32369  qusbas2  32505  qusima  32507  elrspunidl  32534  elrspunsn  32535  evls1fpws  32634  gsummoncoe1fzo  32656  lbsdiflsp0  32699  fedgmullem1  32702  fedgmullem2  32703  mdetpmtr1  32791  mdetlap  32800  xrge0mulc1cn  32909  esumval  33032  esumsnf  33050  esumpcvgval  33064  esumcvg  33072  esumcvgsum  33074  esumsup  33075  ofcfeqd2  33087  meascnbl  33205  sitgval  33319  probmeasb  33417  cndprobprob  33425  dstfrvclim1  33464  ballotlemfval  33476  ballotlemsval  33495  ballotlemieq  33503  plymul02  33545  plymulx0  33546  plymulx  33547  signsplypnf  33549  signstfv  33562  signstfvn  33568  signstfvp  33570  itgexpif  33606  logdivsqrle  33650  ptpconn  34212  cvmliftlem6  34269  cvmliftphtlem  34296  cvmlift3lem5  34302  elmrsubrn  34499  msubfval  34503  msubco  34510  divcnvlin  34690  gg-expcn  35152  gg-divccn  35153  gg-negcncf  35154  gg-dvcnp2  35162  gg-dvmulbr  35163  gg-dvcobr  35164  gg-psercn2  35166  knoppcnlem9  35365  knoppcnlem10  35366  knoppcnlem11  35367  bj-finsumval0  36154  curf  36454  matunitlindflem1  36472  matunitlindflem2  36473  poimirlem3  36479  poimirlem15  36491  poimirlem16  36492  poimirlem17  36493  poimirlem19  36495  poimirlem20  36496  broucube  36510  ovoliunnfl  36518  voliunnfl  36520  volsupnfl  36521  mbfposadd  36523  itg2addnclem  36527  itg2addnclem3  36529  itg2addnc  36530  itgaddnclem2  36535  itgaddnc  36536  iblsubnc  36537  itgsubnc  36538  itgmulc2nclem1  36542  itgmulc2nclem2  36543  itgmulc2nc  36544  itgabsnc  36545  ftc1cnnclem  36547  ftc1anclem3  36551  ftc1anclem5  36553  ftc1anclem6  36554  ftc1anclem8  36556  ftc1anc  36557  ftc2nc  36558  areacirclem1  36564  areacirclem2  36565  areacirclem4  36567  areacirc  36569  upixp  36585  lcmineqlem8  40889  lcmineqlem12  40893  dvrelog2b  40919  dvrelogpow2b  40921  aks4d1p1p6  40926  aks4d1p1p5  40928  sticksstones12a  40961  sticksstones12  40962  sticksstones19  40969  qsalrel  41059  pwsgprod  41111  rhmcomulmpl  41121  evlsvvval  41132  evlsevl  41140  selvvvval  41154  evlselv  41156  fsuppssindlem1  41160  fsuppssind  41162  mhphf  41166  mzpsubst  41471  mzprename  41472  mzpcompact2lem  41474  eldioph2  41485  rabdiophlem2  41525  mendlmod  41920  mendassa  41921  areaquad  41950  fsovcnvlem  42749  hashnzfzclim  43066  expgrowthi  43077  expgrowth  43079  uzmptshftfval  43090  dvradcnv2  43091  binomcxplemrat  43094  binomcxplemfrat  43095  binomcxplemradcnv  43096  binomcxplemdvbinom  43097  binomcxplemcvg  43098  binomcxplemdvsum  43099  binomcxplemnotnn0  43100  mulc1cncfg  44291  expcnfg  44293  fprodcnlem  44301  clim1fr1  44303  divcnvg  44329  sublimc  44354  reclimc  44355  divlimc  44358  limsupresico  44402  limsuppnfdlem  44403  limsupvaluz  44410  supcnvlimsupmpt  44443  liminfresico  44473  climliminflimsupd  44503  cncfmptssg  44573  negcncfg  44583  cncficcgt0  44590  fprodcncf  44602  fprodsubrecnncnvlem  44609  fprodaddrecnncnvlem  44611  dvsinax  44615  dvasinbx  44622  dvdivf  44624  ioodvbdlimc1lem2  44634  ioodvbdlimc2lem  44636  dvnmptdivc  44640  dvxpaek  44642  dvnxpaek  44644  dvnmul  44645  dvnprodlem2  44649  ibliccsinexp  44653  itgsinexplem1  44656  itgsinexp  44657  iblempty  44667  itgcoscmulx  44671  itgsincmulx  44676  itgioocnicc  44679  iblcncfioo  44680  itgsbtaddcnst  44684  volioofmpt  44696  volicofmpt  44699  stoweidlem4  44706  stirlinglem5  44780  dirkerval  44793  dirkertrigeq  44803  dirkeritg  44804  dirkercncflem2  44806  dirkercncflem4  44808  fourierdlem16  44825  fourierdlem18  44827  fourierdlem21  44830  fourierdlem22  44831  fourierdlem28  44837  fourierdlem39  44848  fourierdlem40  44849  fourierdlem41  44850  fourierdlem53  44861  fourierdlem56  44864  fourierdlem57  44865  fourierdlem60  44868  fourierdlem61  44869  fourierdlem68  44876  fourierdlem73  44881  fourierdlem74  44882  fourierdlem75  44883  fourierdlem76  44884  fourierdlem78  44886  fourierdlem81  44889  fourierdlem82  44890  fourierdlem83  44891  fourierdlem84  44892  fourierdlem85  44893  fourierdlem88  44896  fourierdlem90  44898  fourierdlem92  44900  fourierdlem93  44901  fourierdlem95  44903  fourierdlem97  44905  fourierdlem101  44909  fourierdlem103  44911  fourierdlem104  44912  fourierdlem111  44919  fourierdlem112  44920  sqwvfoura  44930  sqwvfourb  44931  fouriersw  44933  elaa2lem  44935  etransclem4  44940  etransclem17  44953  etransclem18  44954  etransclem32  44968  etransclem46  44982  sge0z  45077  sge0revalmpt  45080  sge0tsms  45082  sge0sup  45093  sge0iunmptlemre  45117  sge0iun  45121  sge0xaddlem2  45136  ismeannd  45169  psmeasurelem  45172  meaiuninclem  45182  meaiininclem  45188  caratheodory  45230  isomenndlem  45232  ovnval  45243  hoicvrrex  45258  ovnlecvr  45260  ovncvrrp  45266  ovn0lem  45267  ovnsubaddlem1  45272  hoidmv1lelem2  45294  hoidmv1le  45296  hoidmvlelem3  45299  ovnhoilem2  45304  ovnhoi  45305  ovnlecvr2  45312  ovncvr2  45313  hspmbllem2  45329  ovolval2lem  45345  ovolval3  45349  ovolval5lem1  45354  ovolval5lem2  45355  ovnovollem1  45358  ovnovollem2  45359  vonioolem1  45382  vonicclem1  45385  vonct  45395  smflim  45479  smfinflem  45519  smflimsuplem5  45526  smfliminflem  45532  cfsetsnfsetfv  45753  fundcmpsurbijinjpreimafv  46061  fundcmpsurinjimaid  46065  prdsrngd  46663  fdmdifeqresdif  46970  ply1mulgsumlem2  47021  lincvalsc0  47055  linc0scn0  47057  lincdifsn  47058  lincsum  47063  lincscm  47064  lindslinindimp2lem4  47095  lindslinindsimp2lem5  47096  lincresunit3lem2  47114  1arymaptfo  47282  itcovalpclem1  47309  itcovalpclem2  47310  itcovalt2lem1  47314  itcovalt2lem2  47315  aacllem  47801  amgmwlem  47802