Theorem mpteq2dva 5198

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145   ↦ cmpt 5186

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-opab 5168  df-mpt 5187

This theorem is used by:  mpteq2dv  5199  mpteq2ia  5200  2fvcoidd  7298  offval  7687  offval2  7698  coof  7702  caofinvl  7710  caofcom  7715  caofass  7718  caofdi  7720  caofdir  7721  caonncan  7722  curry1  8101  curry2  8104  mpocurryd  8267  curf  8869  pw2f1olem  9079  mapxpen  9141  xpmapenlem  9142  cantnfp1  9660  cantnflem1d  9667  cantnflem1  9668  cnfcom2lem  9680  dfac12lem1  10146  seqof  14123  seqof2  14124  swrdswrd  14774  repswswrd  14855  repswrevw  14858  revco  14905  ccatco  14906  repsco  14911  ofccat  15042  lo1eq  15655  rlimeq  15656  lo1mul2  15716  o1dif  15717  lo1sub  15718  rlimdiv  15733  caucvgr  15763  sumeq1  15776  fsumrlim  15898  fsumo1  15899  climfsum  15907  geomulcvg  15965  vdwlem8  17080  prmgapprmo  17154  restid2  17515  pwsplusgval  17576  pwsmulrval  17577  pwsvscafval  17580  qusin  17630  xpsaddlem  17659  xpsvsca  17663  catidd  17768  fuclid  18058  fucrid  18059  fucass  18060  setcepi  18177  prf1st  18292  prf2nd  18293  1st2ndprf  18294  curfcl  18320  curfuncf  18326  diag2  18333  curf2ndf  18335  hof2val  18344  hofcllem  18346  hofcl  18347  yonedalem4a  18363  yonedalem4c  18365  yonedalem3b  18367  yonedainv  18369  yonffthlem  18370  prdssgrpd  18835  prdsidlem  18876  prdsmndd  18877  mhmvlin  18909  pwsco2mhm  18942  frmdup3lem  18975  frmdup3  18976  smndex1gid  19013  smndex1gidOLD  19014  smndex1igidOLD  19016  grpinvpropd  19138  prdsinvlem  19172  pwsinvg  19176  pwssub  19177  galactghm  19531  cayleylem1  19539  pmtrprfval  19614  sylow1lem2  19726  sylow3lem1  19754  efginvrel1  19855  frgpup3lem  19904  frgpup3  19905  prdscmnd  19988  iscyggen  20007  gsumval3  20034  gsumcllem  20035  gsumzsplit  20054  gsumsub  20075  gsummptf1o  20090  gsum2d  20099  gsum2d2  20101  gsumxp  20103  prdsgsum  20108  telgsumfz  20117  telgsumfz0  20119  telgsum  20121  dprdfsub  20150  dprdfeq0  20151  dprddisj2  20168  dprd2d2  20173  dpjidcl  20187  ablfaclem2  20215  ablfac2  20218  prdsmgp  20284  prdsrngd  20311  srgbinomlem3  20367  srgbinomlem4  20368  srgbinomlem  20369  gsumdixp  20459  prdsringd  20461  pwsgprod  20470  prdslmodd  21153  mulgrhm2  21691  frgpcyg  21786  freshmansdream  21787  evpmodpmf1o  21809  phlpropd  21868  frlmphl  21994  uvcresum  22006  frlmup1  22011  asclpropd  22112  psrass1lem  22148  psrlinv  22170  psrass1  22178  psrdi  22179  psrdir  22180  psrass23l  22181  psrcom  22182  psrass23  22183  resspsrmul  22190  mplsubrglem  22218  mplmonmul  22252  mplcoe1  22253  mplcoe5  22256  mplcoe4  22287  evlslem3  22296  evlslem1  22298  evlsvvval  22309  rhmcomulmpl  22340  evlsevl  22348  selvvvval  22358  mhpmulcl  22377  psdmplcl  22390  psdadd  22391  psdmul  22394  psdmvr  22397  psrplusgpropd  22460  psropprmul  22462  coe1mul2  22495  coe1tm  22499  coe1tmmul2  22502  coe1tmmul  22503  coe1pwmul  22505  cply1mul  22521  ply1coe  22523  eqcoe1ply1eq  22524  lply1binomsc  22536  evl1gsummon  22590  evls1fpws  22594  mamures  22619  grpvrinv  22621  mamuass  22624  mamudi  22625  mamudir  22626  mamuvs1  22627  mamuvs2  22628  mpomatmul  22668  mamutpos  22680  madetsumid  22683  dmatmul  22719  scmatscm  22735  1mavmul  22770  mavmulass  22771  mvmumamul1  22776  mulmarep1gsum1  22795  mulmarep1gsum2  22796  mdetleib2  22810  mdetfval1  22812  mdet0pr  22814  mdetdiag  22821  mdetdiagid  22822  mdetrlin  22824  mdetrsca  22825  mdetralt  22830  mdetunilem9  22842  gsummatr01  22881  smadiadetlem1a  22885  smadiadetlem3  22890  smadiadetlem4  22891  matunitlindflem1  22901  matunitlindflem2  22902  cpmatmcllem  22943  mat2pmatmul  22956  decpmatmullem  22996  decpmatmul  22997  pmatcollpw1lem2  23000  pmatcollpw  23006  pmatcollpw3lem  23008  pmatcollpwscmat  23016  idpm2idmp  23026  mp2pm2mplem3  23033  mp2pm2mplem4  23034  mp2pm2mplem5  23035  mp2pm2mp  23036  pm2mpghm  23041  pm2mpmhmlem2  23044  monmat2matmon  23049  pm2mp  23050  chpdmat  23066  chpscmat  23067  chpscmatgsumbin  23069  chpscmatgsummon  23070  chp0mat  23071  chpidmat  23072  chfacfscmulgsum  23085  chfacfpmmulgsum  23089  chfacfpmmulgsum2  23090  cayhamlem1  23091  cpmidgsumm2pm  23094  cpmidpmat  23098  cpmadugsumlemB  23099  cpmadugsumlemC  23100  cpmadugsumlemF  23101  cpmadumatpoly  23108  cayhamlem3  23112  cayhamlem4  23113  cayleyhamilton0  23114  cayleyhamiltonALT  23116  neiptopnei  23357  neiptopreu  23358  ptcnplem  23847  cnmpt1t  23891  cnmpt12  23893  cnmptkp  23906  cnmptk1  23907  cnmpt1k  23908  cnmptkk  23909  cnmptk1p  23911  cnmpt2k  23914  qtopeu  23942  pt1hmeo  24032  ptunhmeo  24034  xkocnv  24040  xkohmeo  24041  flfcnp2  24233  cnmpt1plusg  24313  istgp2  24317  tmdmulg  24318  tgpmulg  24319  tmdgsum  24321  subgtgp  24331  symgtgp  24332  tgpconncomp  24339  prdstgpd  24351  tsmsmhm  24372  tsmsadd  24373  tsmssub  24375  tgptsmscls  24376  tsmssplit  24378  tsmsxplem1  24379  tsmsxplem2  24380  cnmpt1vsca  24420  tlmtgp  24422  ustuqtoplem  24465  utopsnneip  24474  ressprdsds  24597  metuval  24775  nmfval0  24816  tngnm  24877  nmoeq0  24962  idnghm  24969  cnmpt1ds  25069  fsumcn  25098  expcn  25100  divccn  25101  divccncf  25134  negcncf  25150  copco  25246  pcopt  25250  pcopt2  25251  pcoass  25252  pi1xfrcnvlem  25284  cnmpt1ip  25475  rrxnm  25619  rrxds  25621  minveclem3b  25656  divcncf  25675  ovolctb  25718  ovoliunnul  25735  voliunlem3  25780  ovolfs2  25799  uniioombllem2  25811  vitalilem4  25839  vitalilem5  25840  ismbf  25856  mbfss  25874  mbfmulc2re  25876  mbfneg  25878  mbfpos  25879  mbfposb  25881  mbfadd  25889  mbfsub  25890  mbfmulc2  25891  mbfinf  25893  mbflimsup  25894  mbflimlem  25895  i1fpos  25934  i1fposd  25935  itg1climres  25942  mbfmul  25954  itg2mulc  25975  itg2i1fseq  25983  itg2cnlem1  25989  itg2cnlem2  25990  itgresr  26006  iblneg  26030  i1fibl  26035  itgitg1  26036  iblsub  26049  itgfsum  26054  itgmulc2lem1  26059  limcmpt  26110  limccnp  26118  limcco  26120  dvreslem  26136  dvres2lem  26137  dvidlem  26142  dvcnp2  26147  dvaddbr  26165  dvmulbr  26166  dvmulf  26170  dvcmulf  26172  dvcobr  26173  dvcof  26175  dvcjbr  26176  dvcj  26177  dvfre  26178  dvexp  26180  dvexp2  26181  dvrec  26182  dvmptcmul  26191  dvmptdivc  26192  dvmptneg  26193  dvmptsub  26194  dvmptre  26196  dvmptim  26197  dvrecg  26200  dvmptdiv  26201  dvmptfsum  26202  dvcnvlem  26203  dvcnv  26204  dvexp3  26205  dvef  26207  dvsincos  26208  dv11cn  26228  lhop2  26242  lhop  26243  ftc2  26271  itgparts  26274  itgsubstlem  26275  mdegfval  26287  mdegmullem  26303  ply1termlem  26428  plypow  26430  plyconst  26431  plyeq0lem  26436  plypf1  26438  plyaddlem1  26439  plymullem1  26440  coeeulem  26450  coeidlem  26463  plyco  26467  coeeq2  26468  0dgr  26471  0dgrb  26472  dgrcolem1  26499  dgrcolem2  26500  plycjlem  26502  plymul02  26510  plyn0mulidp  26511  plymulidp  26512  dvply1  26514  dvply2g  26515  plydiveu  26528  plyremlem  26534  elqaalem3  26553  taylfval  26595  dvtaylp  26606  taylthlem1  26609  taylthlem2  26610  ulmshft  26626  mtestbdd  26641  iblulm  26643  itgulm2  26645  pserulm  26658  psercn2  26659  pserdvlem2  26664  pserdv  26665  pserdv2  26666  abelthlem1  26667  abelthlem3  26669  advlog  26891  advlogexp  26892  dvcxp1  26977  dvcxp2  26978  dvcncxp1  26980  sqrtcn  26987  loglesqrt  26998  dvatan  27172  atantayl2  27175  atantayl3  27176  leibpi  27179  rlimcnp2  27203  efrlim  27206  dfef2  27207  cxp2lim  27213  divsqrtsumlem  27216  lgamgulmlem2  27266  lgamgulm2  27272  lgamcvglem  27276  gamcvg2lem  27295  ftalem7  27315  basellem9  27325  muinv  27429  logfacrlim  27460  logexprlim  27461  dchrmullid  27488  dchrinvcl  27489  lgseisenlem3  27613  lgseisenlem4  27614  chtppilimlem2  27710  chebbnd2  27713  chpchtlim  27715  chpo1ub  27716  rpvmasumlem  27723  dchrmusumlema  27729  dchrvmasumlem1  27731  dchrvmasumiflem2  27738  dchrisum0fno1  27747  rpvmasum2  27748  dchrisum0lema  27750  dchrisum0lem1  27752  dchrisum0lem2a  27753  dchrisum0lem2  27754  dchrisum0  27756  dchrmusumlem  27758  dchrvmasumlem  27759  rpvmasum  27762  rplogsum  27763  logdivsum  27769  mulog2sumlem3  27772  vmalogdivsum2  27774  vmalogdivsum  27775  2vmadivsumlem  27776  logsqvma2  27779  log2sumbnd  27780  selberglem2  27782  selberg3lem1  27793  selberg3  27795  selberg4lem1  27796  selberg4  27797  pntrsumo1  27801  selberg3r  27805  selberg4r  27806  selberg34r  27807  pntrlog2bndlem2  27814  pntrlog2bndlem4  27816  pntrlog2bndlem5  27817  pntrlog2bndlem6  27819  padicabvf  27867  padicabvcxp  27868  mirval  29006  crctcshlem4  30288  clwlknf1oclwwlkn  30554  eucrct2eupth  30725  chscllem4  32121  brafnmul  32432  kbmul  32436  cofmpt2  33107  ofresid  33115  ofoprabco  33137  fmptunsnop  33172  fcobijfs  33192  fcobijfs2  33193  gsummpt2d  33489  gsummptres  33492  gsummptres2  33493  gsummptf1od  33495  gsummptp1  33497  gsummptfsf1o  33500  gsumfs2d  33501  gsumpart  33503  gsumhashmul  33507  gsummulsubdishift1  33508  gsummulsubdishift2  33509  gsumwrd2dccat  33518  fzto1st1  33542  fzto1st  33543  elrgspnlem1  33682  elrgspnlem2  33683  elrgspnlem3  33684  elrgspnlem4  33685  elrgspnsubrunlem1  33687  elrgspnsubrunlem2  33688  qusbas2  33835  qusima  33837  elrspunidl  33856  elrspunsn  33857  rprmdvdsprod  33944  ressply1evls1  33975  evl1deg1  33986  evl1deg2  33987  evl1deg3  33988  gsummoncoe1fzo  34007  mplasclco  34026  selvply1rhmlemb  34029  selvply1rhmlem2  34031  selvply1rhmlem4  34033  selvply1rhm0  34036  mplmulmvr  34049  evlextv  34052  mplvrpmga  34055  mplvrpmmhm  34056  mplvrpmrhm  34057  psrgsum  34058  psrmonmul  34060  issply  34071  esplyfval0  34074  esplyfval3  34082  esplyfval1  34083  esplyfvaln  34084  esplyind  34085  vietalem  34089  lbsdiflsp0  34136  fedgmullem1  34139  fedgmullem2  34140  fldextrspunlsplem  34183  fldextrspunlsp  34184  extdgfialglem2  34203  mdetpmtr1  34333  mdetlap  34342  xrge0mulc1cn  34451  esumval  34556  esumsnf  34574  esumpcvgval  34588  esumcvg  34596  esumcvgsum  34598  esumsup  34599  ofcfeqd2  34611  meascnbl  34730  sitgval  34843  probmeasb  34941  cndprobprob  34949  dstfrvclim1  34989  ballotlemfval  35001  ballotlemsval  35020  ballotlemieq  35028  signsplypnf  35058  signstfv  35071  signstfvn  35077  signstfvp  35079  itgexpif  35114  logdivsqrle  35158  ptpconn  35812  cvmliftlem6  35869  cvmliftphtlem  35896  cvmlift3lem5  35902  elmrsubrn  36099  msubfval  36103  msubco  36110  divcnvlin  36312  knoppcnlem9  37198  knoppcnlem10  37199  knoppcnlem11  37200  bj-finsumval0  38037  poimirlem3  38372  poimirlem15  38384  poimirlem16  38385  poimirlem17  38386  poimirlem19  38388  poimirlem20  38389  broucube  38403  ovoliunnfl  38411  voliunnfl  38413  volsupnfl  38414  mbfposadd  38416  itg2addnclem  38420  itg2addnclem3  38422  itg2addnc  38423  itgaddnclem2  38428  itgaddnc  38429  iblsubnc  38430  itgsubnc  38431  itgmulc2nclem1  38435  itgmulc2nclem2  38436  itgmulc2nc  38437  itgabsnc  38438  ftc1cnnclem  38440  ftc1anclem3  38444  ftc1anclem5  38446  ftc1anclem6  38447  ftc1anclem8  38449  ftc1anc  38450  ftc2nc  38451  areacirclem1  38457  areacirclem2  38458  areacirclem4  38460  areacirc  38462  upixp  38479  lcmineqlem8  42902  lcmineqlem12  42906  dvrelog2b  42932  dvrelogpow2b  42934  aks4d1p1p6  42939  aks4d1p1p5  42941  aks6d1c1  42982  aks6d1c5lem3  43003  sticksstones12a  43023  sticksstones12  43024  sticksstones19  43031  aks6d1c6lem1  43036  aks6d1c6lem4  43039  aks6d1c7lem3  43048  qsalrel  43108  rhmcomulpsr  43428  evlselv  43435  fsuppssindlem1  43437  fsuppssind  43439  mhphf  43443  mzpsubst  43593  mzprename  43594  mzpcompact2lem  43596  eldioph2  43607  rabdiophlem2  43643  mendlmod  44030  mendassa  44031  areaquad  44057  fsovcnvlem  44853  hashnzfzclim  45146  expgrowthi  45157  expgrowth  45159  uzmptshftfval  45170  dvradcnv2  45171  binomcxplemrat  45174  binomcxplemfrat  45175  binomcxplemradcnv  45176  binomcxplemdvbinom  45177  binomcxplemcvg  45178  binomcxplemdvsum  45179  binomcxplemnotnn0  45180  mulc1cncfg  46419  expcnfg  46421  fprodcnlem  46429  clim1fr1  46431  divcnvg  46457  sublimc  46480  reclimc  46481  divlimc  46484  limsupresico  46528  limsuppnfdlem  46529  limsupvaluz  46536  supcnvlimsupmpt  46569  liminfresico  46599  climliminflimsupd  46629  cncfmptssg  46699  negcncfg  46709  cncficcgt0  46716  fprodcncf  46728  fprodsubrecnncnvlem  46735  fprodaddrecnncnvlem  46737  dvsinax  46741  dvasinbx  46748  dvdivf  46750  ioodvbdlimc1lem2  46760  ioodvbdlimc2lem  46762  dvnmptdivc  46766  dvxpaek  46768  dvnxpaek  46770  dvnmul  46771  dvnprodlem2  46775  ibliccsinexp  46779  itgsinexplem1  46782  itgsinexp  46783  iblempty  46793  itgcoscmulx  46797  itgsincmulx  46802  itgioocnicc  46805  iblcncfioo  46806  itgsbtaddcnst  46810  volioofmpt  46822  volicofmpt  46825  stoweidlem4  46832  stirlinglem5  46906  dirkerval  46919  dirkertrigeq  46929  dirkeritg  46930  dirkercncflem2  46932  dirkercncflem4  46934  fourierdlem16  46951  fourierdlem18  46953  fourierdlem21  46956  fourierdlem22  46957  fourierdlem28  46963  fourierdlem39  46974  fourierdlem40  46975  fourierdlem41  46976  fourierdlem53  46987  fourierdlem56  46990  fourierdlem57  46991  fourierdlem60  46994  fourierdlem61  46995  fourierdlem68  47002  fourierdlem73  47007  fourierdlem74  47008  fourierdlem75  47009  fourierdlem76  47010  fourierdlem78  47012  fourierdlem81  47015  fourierdlem82  47016  fourierdlem83  47017  fourierdlem84  47018  fourierdlem85  47019  fourierdlem88  47022  fourierdlem90  47024  fourierdlem92  47026  fourierdlem93  47027  fourierdlem95  47029  fourierdlem97  47031  fourierdlem101  47035  fourierdlem103  47037  fourierdlem104  47038  fourierdlem111  47045  fourierdlem112  47046  sqwvfoura  47056  sqwvfourb  47057  fouriersw  47059  elaa2lem  47061  etransclem4  47066  etransclem17  47079  etransclem18  47080  etransclem32  47094  etransclem46  47108  sge0z  47203  sge0revalmpt  47206  sge0tsms  47208  sge0sup  47219  sge0iunmptlemre  47243  sge0iun  47247  sge0xaddlem2  47262  ismeannd  47295  psmeasurelem  47298  meaiuninclem  47308  meaiininclem  47314  caratheodory  47356  isomenndlem  47358  ovnval  47369  hoicvrrex  47384  ovnlecvr  47386  ovncvrrp  47392  ovn0lem  47393  ovnsubaddlem1  47398  hoidmv1lelem2  47420  hoidmv1le  47422  hoidmvlelem3  47425  ovnhoilem2  47430  ovnhoi  47431  ovnlecvr2  47438  ovncvr2  47439  hspmbllem2  47455  ovolval2lem  47471  ovolval3  47475  ovolval5lem1  47480  ovolval5lem2  47481  ovnovollem1  47484  ovnovollem2  47485  vonioolem1  47508  vonicclem1  47511  vonct  47521  smflim  47605  smfinflem  47645  smflimsuplem5  47652  smfliminflem  47658  cfsetsnfsetfv  47945  fundcmpsurbijinjpreimafv  48307  fundcmpsurinjimaid  48311  fdmdifeqresdif  49272  ply1mulgsumlem2  49317  lincvalsc0  49351  linc0scn0  49353  lincdifsn  49354  lincsum  49359  lincscm  49360  lindslinindimp2lem4  49391  lindslinindsimp2lem5  49392  lincresunit3lem2  49410  1arymaptfo  49573  itcovalpclem1  49600  itcovalpclem2  49601  itcovalt2lem1  49605  itcovalt2lem2  49606  tposcurf1  50225  tposcurf2  50226  diag1  50230  fuco22  50265  fucocolem2  50280  fucocolem3  50281  fucocolem4  50282  fucoco  50283  fucolid  50287  fucorid  50288  postcofval  50290  precofval  50293  precofvalALT  50294  precofval2  50295  fucoppcco  50335  islmd  50591  iscmd  50592  aacllem  50772  veronesematrowd  50814  veronesematrowexpd  50815  veroquadmodzerod  50817  amgmwlem  50820