Theorem mpteq2dva 5214

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2108   ↦ cmpt 5201

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 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-opab 5182  df-mpt 5202

This theorem is referenced by:  mpteq2dv  5215  mpteq2ia  5216  2fvcoidd  7289  offval  7678  offval2  7689  coof  7693  caofinvl  7701  caofcom  7706  caofass  7709  caofdi  7711  caofdir  7712  caonncan  7713  curry1  8101  curry2  8104  mpocurryd  8266  pw2f1olem  9088  mapxpen  9155  xpmapenlem  9156  cantnfp1  9693  cantnflem1d  9700  cantnflem1  9701  cnfcom2lem  9713  dfac12lem1  10156  seqof  14075  seqof2  14076  swrdswrd  14721  repswswrd  14800  repswrevw  14803  revco  14851  ccatco  14852  repsco  14857  ofccat  14986  lo1eq  15582  rlimeq  15583  lo1mul2  15643  o1dif  15644  lo1sub  15645  rlimdiv  15660  caucvgr  15690  sumeq1  15703  fsumrlim  15825  fsumo1  15826  climfsum  15834  geomulcvg  15890  vdwlem8  17006  prmgapprmo  17080  restid2  17442  pwsplusgval  17502  pwsmulrval  17503  pwsvscafval  17506  qusin  17556  xpsaddlem  17585  xpsvsca  17589  catidd  17690  fuclid  17980  fucrid  17981  fucass  17982  setcepi  18099  prf1st  18214  prf2nd  18215  1st2ndprf  18216  curfcl  18242  curfuncf  18248  diag2  18255  curf2ndf  18257  hof2val  18266  hofcllem  18268  hofcl  18269  yonedalem4a  18285  yonedalem4c  18287  yonedalem3b  18289  yonedainv  18291  yonffthlem  18292  prdssgrpd  18709  prdsidlem  18745  prdsmndd  18746  mhmvlin  18777  pwsco2mhm  18809  frmdup3lem  18842  frmdup3  18843  smndex1gid  18879  smndex1igid  18880  grpinvpropd  18996  prdsinvlem  19030  pwsinvg  19034  pwssub  19035  galactghm  19383  cayleylem1  19391  pmtrprfval  19466  sylow1lem2  19578  sylow3lem1  19606  efginvrel1  19707  frgpup3lem  19756  frgpup3  19757  prdscmnd  19840  iscyggen  19859  gsumval3  19886  gsumcllem  19887  gsumzsplit  19906  gsumsub  19927  gsummptf1o  19942  gsum2d  19951  gsum2d2  19953  gsumxp  19955  prdsgsum  19960  telgsumfz  19969  telgsumfz0  19971  telgsum  19973  dprdfsub  20002  dprdfeq0  20003  dprddisj2  20020  dprd2d2  20025  dpjidcl  20039  ablfaclem2  20067  ablfac2  20070  prdsmgp  20109  prdsrngd  20134  srgbinomlem3  20186  srgbinomlem4  20187  srgbinomlem  20188  gsumdixp  20277  prdsringd  20279  prdslmodd  20924  mulgrhm2  21437  frgpcyg  21532  freshmansdream  21533  evpmodpmf1o  21554  phlpropd  21613  frlmphl  21739  uvcresum  21751  frlmup1  21756  asclpropd  21855  psrass1lem  21890  psrlinv  21913  psrass1  21922  psrdi  21923  psrdir  21924  psrass23l  21925  psrcom  21926  psrass23  21927  resspsrmul  21934  mplsubrglem  21962  mplmonmul  21992  mplcoe1  21993  mplcoe5  21996  mplcoe4  22027  evlslem3  22036  evlslem1  22038  mhpmulcl  22085  psdmplcl  22098  psdadd  22099  psdmul  22102  psdmvr  22105  psrplusgpropd  22169  psropprmul  22171  coe1mul2  22204  coe1tm  22208  coe1tmmul2  22211  coe1tmmul  22212  coe1pwmul  22214  cply1mul  22232  ply1coe  22234  eqcoe1ply1eq  22235  lply1binomsc  22247  evl1gsummon  22301  evls1fpws  22305  rhmcomulmpl  22318  mamures  22333  grpvrinv  22335  mamuass  22338  mamudi  22339  mamudir  22340  mamuvs1  22341  mamuvs2  22342  mpomatmul  22382  mamutpos  22394  madetsumid  22397  dmatmul  22433  scmatscm  22449  1mavmul  22484  mavmulass  22485  mvmumamul1  22490  mulmarep1gsum1  22509  mulmarep1gsum2  22510  mdetleib2  22524  mdetfval1  22526  mdet0pr  22528  mdetdiag  22535  mdetdiagid  22536  mdetrlin  22538  mdetrsca  22539  mdetralt  22544  mdetunilem9  22556  gsummatr01  22595  smadiadetlem1a  22599  smadiadetlem3  22604  smadiadetlem4  22605  cpmatmcllem  22654  mat2pmatmul  22667  decpmatmullem  22707  decpmatmul  22708  pmatcollpw1lem2  22711  pmatcollpw  22717  pmatcollpw3lem  22719  pmatcollpwscmat  22727  idpm2idmp  22737  mp2pm2mplem3  22744  mp2pm2mplem4  22745  mp2pm2mplem5  22746  mp2pm2mp  22747  pm2mpghm  22752  pm2mpmhmlem2  22755  monmat2matmon  22760  pm2mp  22761  chpdmat  22777  chpscmat  22778  chpscmatgsumbin  22780  chpscmatgsummon  22781  chp0mat  22782  chpidmat  22783  chfacfscmulgsum  22796  chfacfpmmulgsum  22800  chfacfpmmulgsum2  22801  cayhamlem1  22802  cpmidgsumm2pm  22805  cpmidpmat  22809  cpmadugsumlemB  22810  cpmadugsumlemC  22811  cpmadugsumlemF  22812  cpmadumatpoly  22819  cayhamlem3  22823  cayhamlem4  22824  cayleyhamilton0  22825  cayleyhamiltonALT  22827  neiptopnei  23068  neiptopreu  23069  ptcnplem  23557  cnmpt1t  23601  cnmpt12  23603  cnmptkp  23616  cnmptk1  23617  cnmpt1k  23618  cnmptkk  23619  cnmptk1p  23621  cnmpt2k  23624  qtopeu  23652  pt1hmeo  23742  ptunhmeo  23744  xkocnv  23750  xkohmeo  23751  flfcnp2  23943  cnmpt1plusg  24023  istgp2  24027  tmdmulg  24028  tgpmulg  24029  tmdgsum  24031  subgtgp  24041  symgtgp  24042  tgpconncomp  24049  prdstgpd  24061  tsmsmhm  24082  tsmsadd  24083  tsmssub  24085  tgptsmscls  24086  tsmssplit  24088  tsmsxplem1  24089  tsmsxplem2  24090  cnmpt1vsca  24130  tlmtgp  24132  ustuqtoplem  24176  utopsnneip  24185  ressprdsds  24308  metuval  24486  nmfval0  24527  tngnm  24588  nmoeq0  24673  idnghm  24680  cnmpt1ds  24780  fsumcn  24810  expcn  24812  divccn  24813  expcnOLD  24814  divccnOLD  24815  divccncf  24848  negcncf  24864  negcncfOLD  24865  copco  24967  pcopt  24971  pcopt2  24972  pcoass  24973  pi1xfrcnvlem  25005  cnmpt1ip  25197  rrxnm  25341  rrxds  25343  minveclem3b  25378  divcncf  25398  ovolctb  25441  ovoliunnul  25458  voliunlem3  25503  ovolfs2  25522  uniioombllem2  25534  vitalilem4  25562  vitalilem5  25563  ismbf  25579  mbfss  25597  mbfmulc2re  25599  mbfneg  25601  mbfpos  25602  mbfposb  25604  mbfadd  25612  mbfsub  25613  mbfmulc2  25614  mbfinf  25616  mbflimsup  25617  mbflimlem  25618  i1fpos  25657  i1fposd  25658  itg1climres  25665  mbfmul  25677  itg2mulc  25698  itg2i1fseq  25706  itg2cnlem1  25712  itg2cnlem2  25713  itgresr  25730  iblneg  25754  i1fibl  25759  itgitg1  25760  iblsub  25773  itgfsum  25778  itgmulc2lem1  25783  limcmpt  25834  limccnp  25842  limcco  25844  dvreslem  25860  dvres2lem  25861  dvidlem  25866  dvcnp2  25871  dvcnp2OLD  25872  dvaddbr  25890  dvmulbr  25891  dvmulbrOLD  25892  dvmulf  25896  dvcmulf  25898  dvcobr  25899  dvcobrOLD  25900  dvcof  25902  dvcjbr  25903  dvcj  25904  dvfre  25905  dvexp  25907  dvexp2  25908  dvrec  25909  dvmptcmul  25918  dvmptdivc  25919  dvmptneg  25920  dvmptsub  25921  dvmptre  25923  dvmptim  25924  dvrecg  25927  dvmptdiv  25928  dvmptfsum  25929  dvcnvlem  25930  dvcnv  25931  dvexp3  25932  dvef  25934  dvsincos  25935  dv11cn  25956  lhop2  25970  lhop  25971  ftc2  26001  itgparts  26004  itgsubstlem  26005  mdegfval  26017  mdegmullem  26033  ply1termlem  26158  plypow  26160  plyconst  26161  plyeq0lem  26165  plypf1  26167  plyaddlem1  26168  plymullem1  26169  coeeulem  26179  coeidlem  26192  plyco  26196  coeeq2  26197  0dgr  26200  0dgrb  26201  dgrcolem1  26229  dgrcolem2  26230  plycjlem  26232  dvply1  26241  dvply2g  26242  dvply2gOLD  26243  plydiveu  26256  plyremlem  26262  elqaalem3  26279  taylfval  26316  dvtaylp  26328  taylthlem1  26331  taylthlem2  26332  taylthlem2OLD  26333  ulmshft  26349  mtestbdd  26364  iblulm  26366  itgulm2  26368  pserulm  26381  psercn2  26382  psercn2OLD  26383  pserdvlem2  26388  pserdv  26389  pserdv2  26390  abelthlem1  26391  abelthlem3  26393  advlog  26613  advlogexp  26614  dvcxp1  26699  dvcxp2  26700  dvcncxp1  26702  sqrtcn  26710  loglesqrt  26721  dvatan  26895  atantayl2  26898  atantayl3  26899  leibpi  26902  rlimcnp2  26926  efrlim  26929  efrlimOLD  26930  dfef2  26931  cxp2lim  26937  divsqrtsumlem  26940  lgamgulmlem2  26990  lgamgulm2  26996  lgamcvglem  27000  gamcvg2lem  27019  ftalem7  27039  basellem9  27049  muinv  27153  logfacrlim  27185  logexprlim  27186  dchrmullid  27213  dchrinvcl  27214  lgseisenlem3  27338  lgseisenlem4  27339  chtppilimlem2  27435  chebbnd2  27438  chpchtlim  27440  chpo1ub  27441  rpvmasumlem  27448  dchrmusumlema  27454  dchrvmasumlem1  27456  dchrvmasumiflem2  27463  dchrisum0fno1  27472  rpvmasum2  27473  dchrisum0lema  27475  dchrisum0lem1  27477  dchrisum0lem2a  27478  dchrisum0lem2  27479  dchrisum0  27481  dchrmusumlem  27483  dchrvmasumlem  27484  rpvmasum  27487  rplogsum  27488  logdivsum  27494  mulog2sumlem3  27497  vmalogdivsum2  27499  vmalogdivsum  27500  2vmadivsumlem  27501  logsqvma2  27504  log2sumbnd  27505  selberglem2  27507  selberg3lem1  27518  selberg3  27520  selberg4lem1  27521  selberg4  27522  pntrsumo1  27526  selberg3r  27530  selberg4r  27531  selberg34r  27532  pntrlog2bndlem2  27539  pntrlog2bndlem4  27541  pntrlog2bndlem5  27542  pntrlog2bndlem6  27544  padicabvf  27592  padicabvcxp  27593  mirval  28580  crctcshlem4  29748  clwlknf1oclwwlkn  30011  eucrct2eupth  30172  chscllem4  31567  brafnmul  31878  kbmul  31882  cofmpt2  32558  ofresid  32566  ofoprabco  32588  fmptunsnop  32623  fcobijfs  32646  gsummpt2d  32989  gsummptres  32992  gsummptres2  32993  gsummptfsf1o  32994  gsumfs2d  32995  gsumpart  32997  gsumhashmul  33001  gsumwrd2dccat  33007  fzto1st1  33059  fzto1st  33060  elrgspnlem1  33183  elrgspnlem2  33184  elrgspnlem3  33185  elrgspnlem4  33186  elrgspnsubrunlem1  33188  elrgspnsubrunlem2  33189  qusbas2  33367  qusima  33369  elrspunidl  33389  elrspunsn  33390  rprmdvdsprod  33495  ressply1evls1  33524  evl1deg1  33535  evl1deg2  33536  evl1deg3  33537  gsummoncoe1fzo  33553  lbsdiflsp0  33612  fedgmullem1  33615  fedgmullem2  33616  fldextrspunlsplem  33660  fldextrspunlsp  33661  mdetpmtr1  33800  mdetlap  33809  xrge0mulc1cn  33918  esumval  34023  esumsnf  34041  esumpcvgval  34055  esumcvg  34063  esumcvgsum  34065  esumsup  34066  ofcfeqd2  34078  meascnbl  34196  sitgval  34310  probmeasb  34408  cndprobprob  34416  dstfrvclim1  34456  ballotlemfval  34468  ballotlemsval  34487  ballotlemieq  34495  plymul02  34524  plymulx0  34525  plymulx  34526  signsplypnf  34528  signstfv  34541  signstfvn  34547  signstfvp  34549  itgexpif  34584  logdivsqrle  34628  ptpconn  35201  cvmliftlem6  35258  cvmliftphtlem  35285  cvmlift3lem5  35291  elmrsubrn  35488  msubfval  35492  msubco  35499  divcnvlin  35696  knoppcnlem9  36465  knoppcnlem10  36466  knoppcnlem11  36467  bj-finsumval0  37249  curf  37568  matunitlindflem1  37586  matunitlindflem2  37587  poimirlem3  37593  poimirlem15  37605  poimirlem16  37606  poimirlem17  37607  poimirlem19  37609  poimirlem20  37610  broucube  37624  ovoliunnfl  37632  voliunnfl  37634  volsupnfl  37635  mbfposadd  37637  itg2addnclem  37641  itg2addnclem3  37643  itg2addnc  37644  itgaddnclem2  37649  itgaddnc  37650  iblsubnc  37651  itgsubnc  37652  itgmulc2nclem1  37656  itgmulc2nclem2  37657  itgmulc2nc  37658  itgabsnc  37659  ftc1cnnclem  37661  ftc1anclem3  37665  ftc1anclem5  37667  ftc1anclem6  37668  ftc1anclem8  37670  ftc1anc  37671  ftc2nc  37672  areacirclem1  37678  areacirclem2  37679  areacirclem4  37681  areacirc  37683  upixp  37699  lcmineqlem8  41995  lcmineqlem12  41999  dvrelog2b  42025  dvrelogpow2b  42027  aks4d1p1p6  42032  aks4d1p1p5  42034  aks6d1c1  42075  aks6d1c5lem3  42096  sticksstones12a  42116  sticksstones12  42117  sticksstones19  42124  aks6d1c6lem1  42129  aks6d1c6lem4  42132  aks6d1c7lem3  42141  qsalrel  42238  pwsgprod  42514  rhmcomulpsr  42521  evlsvvval  42533  evlsevl  42541  selvvvval  42555  evlselv  42557  fsuppssindlem1  42561  fsuppssind  42563  mhphf  42567  mzpsubst  42718  mzprename  42719  mzpcompact2lem  42721  eldioph2  42732  rabdiophlem2  42772  mendlmod  43160  mendassa  43161  areaquad  43187  fsovcnvlem  43984  hashnzfzclim  44294  expgrowthi  44305  expgrowth  44307  uzmptshftfval  44318  dvradcnv2  44319  binomcxplemrat  44322  binomcxplemfrat  44323  binomcxplemradcnv  44324  binomcxplemdvbinom  44325  binomcxplemcvg  44326  binomcxplemdvsum  44327  binomcxplemnotnn0  44328  mulc1cncfg  45566  expcnfg  45568  fprodcnlem  45576  clim1fr1  45578  divcnvg  45604  sublimc  45629  reclimc  45630  divlimc  45633  limsupresico  45677  limsuppnfdlem  45678  limsupvaluz  45685  supcnvlimsupmpt  45718  liminfresico  45748  climliminflimsupd  45778  cncfmptssg  45848  negcncfg  45858  cncficcgt0  45865  fprodcncf  45877  fprodsubrecnncnvlem  45884  fprodaddrecnncnvlem  45886  dvsinax  45890  dvasinbx  45897  dvdivf  45899  ioodvbdlimc1lem2  45909  ioodvbdlimc2lem  45911  dvnmptdivc  45915  dvxpaek  45917  dvnxpaek  45919  dvnmul  45920  dvnprodlem2  45924  ibliccsinexp  45928  itgsinexplem1  45931  itgsinexp  45932  iblempty  45942  itgcoscmulx  45946  itgsincmulx  45951  itgioocnicc  45954  iblcncfioo  45955  itgsbtaddcnst  45959  volioofmpt  45971  volicofmpt  45974  stoweidlem4  45981  stirlinglem5  46055  dirkerval  46068  dirkertrigeq  46078  dirkeritg  46079  dirkercncflem2  46081  dirkercncflem4  46083  fourierdlem16  46100  fourierdlem18  46102  fourierdlem21  46105  fourierdlem22  46106  fourierdlem28  46112  fourierdlem39  46123  fourierdlem40  46124  fourierdlem41  46125  fourierdlem53  46136  fourierdlem56  46139  fourierdlem57  46140  fourierdlem60  46143  fourierdlem61  46144  fourierdlem68  46151  fourierdlem73  46156  fourierdlem74  46157  fourierdlem75  46158  fourierdlem76  46159  fourierdlem78  46161  fourierdlem81  46164  fourierdlem82  46165  fourierdlem83  46166  fourierdlem84  46167  fourierdlem85  46168  fourierdlem88  46171  fourierdlem90  46173  fourierdlem92  46175  fourierdlem93  46176  fourierdlem95  46178  fourierdlem97  46180  fourierdlem101  46184  fourierdlem103  46186  fourierdlem104  46187  fourierdlem111  46194  fourierdlem112  46195  sqwvfoura  46205  sqwvfourb  46206  fouriersw  46208  elaa2lem  46210  etransclem4  46215  etransclem17  46228  etransclem18  46229  etransclem32  46243  etransclem46  46257  sge0z  46352  sge0revalmpt  46355  sge0tsms  46357  sge0sup  46368  sge0iunmptlemre  46392  sge0iun  46396  sge0xaddlem2  46411  ismeannd  46444  psmeasurelem  46447  meaiuninclem  46457  meaiininclem  46463  caratheodory  46505  isomenndlem  46507  ovnval  46518  hoicvrrex  46533  ovnlecvr  46535  ovncvrrp  46541  ovn0lem  46542  ovnsubaddlem1  46547  hoidmv1lelem2  46569  hoidmv1le  46571  hoidmvlelem3  46574  ovnhoilem2  46579  ovnhoi  46580  ovnlecvr2  46587  ovncvr2  46588  hspmbllem2  46604  ovolval2lem  46620  ovolval3  46624  ovolval5lem1  46629  ovolval5lem2  46630  ovnovollem1  46633  ovnovollem2  46634  vonioolem1  46657  vonicclem1  46660  vonct  46670  smflim  46754  smfinflem  46794  smflimsuplem5  46801  smfliminflem  46807  cfsetsnfsetfv  47034  fundcmpsurbijinjpreimafv  47369  fundcmpsurinjimaid  47373  fdmdifeqresdif  48265  ply1mulgsumlem2  48311  lincvalsc0  48345  linc0scn0  48347  lincdifsn  48348  lincsum  48353  lincscm  48354  lindslinindimp2lem4  48385  lindslinindsimp2lem5  48386  lincresunit3lem2  48404  1arymaptfo  48571  itcovalpclem1  48598  itcovalpclem2  48599  itcovalt2lem1  48603  itcovalt2lem2  48604  tposcurf1  49158  tposcurf2  49159  diag1  49163  fuco22  49198  fucocolem2  49213  fucocolem3  49214  fucocolem4  49215  fucoco  49216  fucolid  49220  fucorid  49221  postcofval  49223  precofval  49226  precofvalALT  49227  precofval2  49228  islmd  49483  iscmd  49484  aacllem  49613  amgmwlem  49614