Theorem mpteq2dva 5125

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-12 2179  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-tru 1545  df-ex 1787  df-nf 1791  df-sb 2075  df-clab 2717  df-cleq 2730  df-clel 2811  df-ral 3058  df-opab 5093  df-mpt 5111

This theorem is referenced by:  mpteq2dv  5126  2fvcoidd  7064  offval  7433  offval2  7444  caofinvl  7454  caofcom  7459  caofass  7461  caofdi  7463  caofdir  7464  caonncan  7465  curry1  7825  curry2  7828  mpocurryd  7964  pw2f1olem  8670  mapxpen  8733  xpmapenlem  8734  cantnfp1  9217  cantnflem1d  9224  cantnflem1  9225  cnfcom2lem  9237  dfac12lem1  9643  seqof  13519  seqof2  13520  swrdswrd  14156  repswswrd  14235  repswrevw  14238  revco  14285  ccatco  14286  repsco  14291  ofccat  14418  lo1eq  15015  rlimeq  15016  lo1mul2  15076  o1dif  15077  lo1sub  15078  rlimdiv  15095  caucvgr  15125  sumeq1  15138  fsumrlim  15259  fsumo1  15260  climfsum  15268  geomulcvg  15324  vdwlem8  16424  prmgapprmo  16498  restid2  16807  pwsplusgval  16866  pwsmulrval  16867  pwsvscafval  16870  qusin  16920  xpsaddlem  16949  xpsvsca  16953  catidd  17054  fuclid  17341  fucrid  17342  fucass  17343  setcepi  17460  prf1st  17570  prf2nd  17571  1st2ndprf  17572  curfcl  17598  curfuncf  17604  diag2  17611  curf2ndf  17613  hof2val  17622  hofcllem  17624  hofcl  17625  yonedalem4a  17641  yonedalem4c  17643  yonedalem3b  17645  yonedainv  17647  yonffthlem  17648  prdsidlem  18059  prdsmndd  18060  pwsco2mhm  18113  frmdup3lem  18147  frmdup3  18148  smndex1gid  18184  smndex1igid  18185  grpinvpropd  18292  prdsinvlem  18326  pwsinvg  18330  pwssub  18331  galactghm  18650  cayleylem1  18658  pmtrprfval  18733  sylow1lem2  18842  sylow3lem1  18870  efginvrel1  18972  frgpup3lem  19021  frgpup3  19022  prdscmnd  19100  iscyggen  19118  gsumval3  19146  gsumcllem  19147  gsumzsplit  19166  gsumsub  19187  gsummptf1o  19202  gsum2d  19211  gsum2d2  19213  gsumxp  19215  prdsgsum  19220  telgsumfz  19229  telgsumfz0  19231  telgsum  19233  dprdfsub  19262  dprdfeq0  19263  dprddisj2  19280  dprd2d2  19285  dpjidcl  19299  ablfaclem2  19327  ablfac2  19330  srgbinomlem3  19411  srgbinomlem4  19412  srgbinomlem  19413  gsumdixp  19481  prdsmgp  19482  prdsringd  19484  prdslmodd  19860  mulgrhm2  20319  frgpcyg  20392  evpmodpmf1o  20412  phlpropd  20471  frlmphl  20597  uvcresum  20609  frlmup1  20614  asclpropd  20711  psrass1lemOLD  20753  psrass1lem  20756  psrlinv  20776  psrass1  20784  psrdi  20785  psrdir  20786  psrass23l  20787  psrcom  20788  psrass23  20789  resspsrmul  20796  mplsubrglem  20820  mplmonmul  20847  mplcoe1  20848  mplcoe5  20851  mplcoe4  20883  evlslem3  20894  evlslem1  20896  mhpmulcl  20943  psrplusgpropd  21011  psropprmul  21013  coe1mul2  21044  coe1tm  21048  coe1tmmul2  21051  coe1tmmul  21052  coe1pwmul  21054  cply1mul  21069  ply1coe  21071  eqcoe1ply1eq  21072  lply1binomsc  21082  evl1gsummon  21135  mamures  21143  grpvrinv  21149  mhmvlin  21150  mamuass  21153  mamudi  21154  mamudir  21155  mamuvs1  21156  mamuvs2  21157  mpomatmul  21197  mamutpos  21209  madetsumid  21212  dmatmul  21248  scmatscm  21264  1mavmul  21299  mavmulass  21300  mvmumamul1  21305  mulmarep1gsum1  21324  mulmarep1gsum2  21325  mdetleib2  21339  mdetfval1  21341  mdet0pr  21343  mdetdiag  21350  mdetdiagid  21351  mdetrlin  21353  mdetrsca  21354  mdetralt  21359  mdetunilem9  21371  gsummatr01  21410  smadiadetlem1a  21414  smadiadetlem3  21419  smadiadetlem4  21420  cpmatmcllem  21469  mat2pmatmul  21482  decpmatmullem  21522  decpmatmul  21523  pmatcollpw1lem2  21526  pmatcollpw  21532  pmatcollpw3lem  21534  pmatcollpwscmat  21542  idpm2idmp  21552  mp2pm2mplem3  21559  mp2pm2mplem4  21560  mp2pm2mplem5  21561  mp2pm2mp  21562  pm2mpghm  21567  pm2mpmhmlem2  21570  monmat2matmon  21575  pm2mp  21576  chpdmat  21592  chpscmat  21593  chpscmatgsumbin  21595  chpscmatgsummon  21596  chp0mat  21597  chpidmat  21598  chfacfscmulgsum  21611  chfacfpmmulgsum  21615  chfacfpmmulgsum2  21616  cayhamlem1  21617  cpmidgsumm2pm  21620  cpmidpmat  21624  cpmadugsumlemB  21625  cpmadugsumlemC  21626  cpmadugsumlemF  21627  cpmadumatpoly  21634  cayhamlem3  21638  cayhamlem4  21639  cayleyhamilton0  21640  cayleyhamiltonALT  21642  neiptopnei  21883  neiptopreu  21884  ptcnplem  22372  cnmpt1t  22416  cnmpt12  22418  cnmptkp  22431  cnmptk1  22432  cnmpt1k  22433  cnmptkk  22434  cnmptk1p  22436  cnmpt2k  22439  qtopeu  22467  pt1hmeo  22557  ptunhmeo  22559  xkocnv  22565  xkohmeo  22566  flfcnp2  22758  cnmpt1plusg  22838  istgp2  22842  tmdmulg  22843  tgpmulg  22844  tmdgsum  22846  subgtgp  22856  symgtgp  22857  tgpconncomp  22864  prdstgpd  22876  tsmsmhm  22897  tsmsadd  22898  tsmssub  22900  tgptsmscls  22901  tsmssplit  22903  tsmsxplem1  22904  tsmsxplem2  22905  cnmpt1vsca  22945  tlmtgp  22947  ustuqtoplem  22991  utopsnneip  23000  ressprdsds  23124  metuval  23302  nmfval0  23343  tngnm  23404  nmoeq0  23489  idnghm  23496  cnmpt1ds  23594  fsumcn  23622  expcn  23624  divccn  23625  divccncf  23658  negcncf  23674  copco  23770  pcopt  23774  pcopt2  23775  pcoass  23776  pi1xfrcnvlem  23808  cnmpt1ip  23999  rrxnm  24143  rrxds  24145  minveclem3b  24180  divcncf  24199  ovolctb  24242  ovoliunnul  24259  voliunlem3  24304  ovolfs2  24323  uniioombllem2  24335  vitalilem4  24363  vitalilem5  24364  ismbf  24380  mbfss  24398  mbfmulc2re  24400  mbfneg  24402  mbfpos  24403  mbfposb  24405  mbfadd  24413  mbfsub  24414  mbfmulc2  24415  mbfinf  24417  mbflimsup  24418  mbflimlem  24419  i1fpos  24459  i1fposd  24460  itg1climres  24467  mbfmul  24479  itg2mulc  24500  itg2i1fseq  24508  itg2cnlem1  24514  itg2cnlem2  24515  itgresr  24531  iblneg  24555  i1fibl  24560  itgitg1  24561  iblsub  24574  itgfsum  24579  itgmulc2lem1  24584  limcmpt  24635  limccnp  24643  limcco  24645  dvreslem  24661  dvres2lem  24662  dvidlem  24667  dvcnp2  24672  dvaddbr  24690  dvmulbr  24691  dvmulf  24695  dvcmulf  24697  dvcobr  24698  dvcof  24700  dvcjbr  24701  dvcj  24702  dvfre  24703  dvexp  24705  dvexp2  24706  dvrec  24707  dvmptcmul  24716  dvmptdivc  24717  dvmptneg  24718  dvmptsub  24719  dvmptre  24721  dvmptim  24722  dvrecg  24725  dvmptdiv  24726  dvmptfsum  24727  dvcnvlem  24728  dvcnv  24729  dvexp3  24730  dvef  24732  dvsincos  24733  dv11cn  24753  lhop2  24767  lhop  24768  ftc2  24796  itgparts  24799  itgsubstlem  24800  mdegfval  24815  mdegmullem  24831  ply1termlem  24952  plypow  24954  plyconst  24955  plyeq0lem  24959  plypf1  24961  plyaddlem1  24962  plymullem1  24963  coeeulem  24973  coeidlem  24986  plyco  24990  coeeq2  24991  0dgr  24994  0dgrb  24995  dgrcolem1  25022  dgrcolem2  25023  plycjlem  25025  dvply1  25032  dvply2g  25033  plydiveu  25046  plyremlem  25052  elqaalem3  25069  taylfval  25106  dvtaylp  25117  taylthlem1  25120  taylthlem2  25121  ulmshft  25137  mtestbdd  25152  iblulm  25154  itgulm2  25156  pserulm  25169  psercn2  25170  pserdvlem2  25175  pserdv  25176  pserdv2  25177  abelthlem1  25178  abelthlem3  25180  advlog  25397  advlogexp  25398  dvcxp1  25481  dvcxp2  25482  dvcncxp1  25484  sqrtcn  25491  loglesqrt  25499  dvatan  25673  atantayl2  25676  atantayl3  25677  leibpi  25680  rlimcnp2  25704  efrlim  25707  dfef2  25708  cxp2lim  25714  divsqrtsumlem  25717  lgamgulmlem2  25767  lgamgulm2  25773  lgamcvglem  25777  gamcvg2lem  25796  ftalem7  25816  basellem9  25826  muinv  25930  logfacrlim  25960  logexprlim  25961  dchrmulid2  25988  dchrinvcl  25989  lgseisenlem3  26113  lgseisenlem4  26114  chtppilimlem2  26210  chebbnd2  26213  chpchtlim  26215  chpo1ub  26216  rpvmasumlem  26223  dchrmusumlema  26229  dchrvmasumlem1  26231  dchrvmasumiflem2  26238  dchrisum0fno1  26247  rpvmasum2  26248  dchrisum0lema  26250  dchrisum0lem1  26252  dchrisum0lem2a  26253  dchrisum0lem2  26254  dchrisum0  26256  dchrmusumlem  26258  dchrvmasumlem  26259  rpvmasum  26262  rplogsum  26263  logdivsum  26269  mulog2sumlem3  26272  vmalogdivsum2  26274  vmalogdivsum  26275  2vmadivsumlem  26276  logsqvma2  26279  log2sumbnd  26280  selberglem2  26282  selberg3lem1  26293  selberg3  26295  selberg4lem1  26296  selberg4  26297  pntrsumo1  26301  selberg3r  26305  selberg4r  26306  selberg34r  26307  pntrlog2bndlem2  26314  pntrlog2bndlem4  26316  pntrlog2bndlem5  26317  pntrlog2bndlem6  26319  padicabvf  26367  padicabvcxp  26368  mirval  26601  crctcshlem4  27758  clwlknf1oclwwlkn  28021  eucrct2eupth  28182  chscllem4  29575  brafnmul  29886  kbmul  29890  cofmpt2  30543  ofresid  30553  ofoprabco  30576  fcobijfs  30633  gsummpt2d  30886  gsummptres  30889  gsummptres2  30890  gsumpart  30892  gsumhashmul  30893  fzto1st1  30946  fzto1st  30947  freshmansdream  31061  qusima  31166  elrspunidl  31178  lbsdiflsp0  31279  fedgmullem1  31282  fedgmullem2  31283  mdetpmtr1  31345  mdetlap  31354  xrge0mulc1cn  31463  esumval  31584  esumsnf  31602  esumpcvgval  31616  esumcvg  31624  esumcvgsum  31626  esumsup  31627  ofcfeqd2  31639  meascnbl  31757  sitgval  31869  probmeasb  31967  cndprobprob  31975  dstfrvclim1  32014  ballotlemfval  32026  ballotlemsval  32045  ballotlemieq  32053  plymul02  32095  plymulx0  32096  plymulx  32097  signsplypnf  32099  signstfv  32112  signstfvn  32118  signstfvp  32120  itgexpif  32156  logdivsqrle  32200  ptpconn  32766  cvmliftlem6  32823  cvmliftphtlem  32850  cvmlift3lem5  32856  elmrsubrn  33053  msubfval  33057  msubco  33064  divcnvlin  33269  knoppcnlem9  34319  knoppcnlem10  34320  knoppcnlem11  34321  bj-finsumval0  35077  curf  35378  matunitlindflem1  35396  matunitlindflem2  35397  poimirlem3  35403  poimirlem15  35415  poimirlem16  35416  poimirlem17  35417  poimirlem19  35419  poimirlem20  35420  broucube  35434  ovoliunnfl  35442  voliunnfl  35444  volsupnfl  35445  mbfposadd  35447  itg2addnclem  35451  itg2addnclem3  35453  itg2addnc  35454  itgaddnclem2  35459  itgaddnc  35460  iblsubnc  35461  itgsubnc  35462  itgmulc2nclem1  35466  itgmulc2nclem2  35467  itgmulc2nc  35468  itgabsnc  35469  ftc1cnnclem  35471  ftc1anclem3  35475  ftc1anclem5  35477  ftc1anclem6  35478  ftc1anclem8  35480  ftc1anc  35481  ftc2nc  35482  areacirclem1  35488  areacirclem2  35489  areacirclem4  35491  areacirc  35493  upixp  35510  lcmineqlem8  39664  lcmineqlem12  39668  dvrelog2b  39693  dvrelogpow2b  39695  aks4d1p1p6  39700  aks4d1p1p5  39702  qsalrel  39797  pwsgprod  39850  evlsbagval  39854  fsuppssindlem1  39859  fsuppssind  39861  mhphf  39864  mzpsubst  40142  mzprename  40143  mzpcompact2lem  40145  eldioph2  40156  rabdiophlem2  40196  mendlmod  40590  mendassa  40591  areaquad  40619  fsovcnvlem  41167  hashnzfzclim  41478  expgrowthi  41489  expgrowth  41491  uzmptshftfval  41502  dvradcnv2  41503  binomcxplemrat  41506  binomcxplemfrat  41507  binomcxplemradcnv  41508  binomcxplemdvbinom  41509  binomcxplemcvg  41510  binomcxplemdvsum  41511  binomcxplemnotnn0  41512  mulc1cncfg  42672  expcnfg  42674  fprodcnlem  42682  clim1fr1  42684  divcnvg  42710  sublimc  42735  reclimc  42736  divlimc  42739  limsupresico  42783  limsuppnfdlem  42784  limsupvaluz  42791  supcnvlimsupmpt  42824  liminfresico  42854  climliminflimsupd  42884  cncfmptssg  42954  negcncfg  42964  cncficcgt0  42971  fprodcncf  42983  fprodsubrecnncnvlem  42990  fprodaddrecnncnvlem  42992  dvsinax  42996  dvasinbx  43003  dvdivf  43005  ioodvbdlimc1lem2  43015  ioodvbdlimc2lem  43017  dvnmptdivc  43021  dvxpaek  43023  dvnxpaek  43025  dvnmul  43026  dvnprodlem2  43030  ibliccsinexp  43034  itgsinexplem1  43037  itgsinexp  43038  iblempty  43048  itgcoscmulx  43052  itgsincmulx  43057  itgioocnicc  43060  iblcncfioo  43061  itgsbtaddcnst  43065  volioofmpt  43077  volicofmpt  43080  stoweidlem4  43087  stirlinglem5  43161  dirkerval  43174  dirkertrigeq  43184  dirkeritg  43185  dirkercncflem2  43187  dirkercncflem4  43189  fourierdlem16  43206  fourierdlem18  43208  fourierdlem21  43211  fourierdlem22  43212  fourierdlem28  43218  fourierdlem39  43229  fourierdlem40  43230  fourierdlem41  43231  fourierdlem53  43242  fourierdlem56  43245  fourierdlem57  43246  fourierdlem60  43249  fourierdlem61  43250  fourierdlem68  43257  fourierdlem73  43262  fourierdlem74  43263  fourierdlem75  43264  fourierdlem76  43265  fourierdlem78  43267  fourierdlem81  43270  fourierdlem82  43271  fourierdlem83  43272  fourierdlem84  43273  fourierdlem85  43274  fourierdlem88  43277  fourierdlem90  43279  fourierdlem92  43281  fourierdlem93  43282  fourierdlem95  43284  fourierdlem97  43286  fourierdlem101  43290  fourierdlem103  43292  fourierdlem104  43293  fourierdlem111  43300  fourierdlem112  43301  sqwvfoura  43311  sqwvfourb  43312  fouriersw  43314  elaa2lem  43316  etransclem4  43321  etransclem17  43334  etransclem18  43335  etransclem32  43349  etransclem46  43363  sge0z  43455  sge0revalmpt  43458  sge0tsms  43460  sge0sup  43471  sge0iunmptlemre  43495  sge0iun  43499  sge0xaddlem2  43514  ismeannd  43547  psmeasurelem  43550  meaiuninclem  43560  meaiininclem  43566  caratheodory  43608  isomenndlem  43610  ovnval  43621  hoicvrrex  43636  ovnlecvr  43638  ovncvrrp  43644  ovn0lem  43645  ovnsubaddlem1  43650  hoidmv1lelem2  43672  hoidmv1le  43674  hoidmvlelem3  43677  ovnhoilem2  43682  ovnhoi  43683  ovnlecvr2  43690  ovncvr2  43691  hspmbllem2  43707  ovolval2lem  43723  ovolval3  43727  ovolval5lem1  43732  ovolval5lem2  43733  ovnovollem1  43736  ovnovollem2  43737  vonioolem1  43760  vonicclem1  43763  vonct  43773  smflim  43851  smfinflem  43889  smflimsuplem5  43896  smfliminflem  43902  cfsetsnfsetfv  44089  fundcmpsurbijinjpreimafv  44393  fundcmpsurinjimaid  44397  fdmdifeqresdif  45211  ply1mulgsumlem2  45262  lincvalsc0  45296  linc0scn0  45298  lincdifsn  45299  lincsum  45304  lincscm  45305  lindslinindimp2lem4  45336  lindslinindsimp2lem5  45337  lincresunit3lem2  45355  1arymaptfo  45523  itcovalpclem1  45550  itcovalpclem2  45551  itcovalt2lem1  45555  itcovalt2lem2  45556  aacllem  45958  amgmwlem  45959