Theorem mpteq2dv 5212

Description: An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 23-Aug-2014.)

Hypothesis

Ref	Expression
mpteq2dv.1	⊢ (𝜑 → 𝐵 = 𝐶)

Assertion

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

Distinct variable group:   𝜑,𝑥

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

Proof of Theorem mpteq2dv

Step	Hyp	Ref	Expression
1		mpteq2dv.1	. . 3 ⊢ (𝜑 → 𝐵 = 𝐶)
2	1	adantr 481	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)
3	2	mpteq2dva 5210	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106   ↦ cmpt 5193

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 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-opab 5173  df-mpt 5194

This theorem is referenced by:  ofeqd  7624  mpocurryvald  8206  rdgeq1  8362  rdgeq2  8363  omv  8463  oev  8465  oieq1  9457  oieq2  9458  cantnflem1  9634  wunex2  10683  wuncval2  10692  rpnnen1  12917  seqof2  13976  relexpsucnnr  14922  relexp1g  14923  limsupval  15368  sumeq2w  15588  sumeq2ii  15589  cbvsum  15591  summo  15613  fsum  15616  fsumrlim  15707  fsumo1  15708  prodeq2w  15806  prodmo  15830  fprod  15835  bpolylem  15942  rpnnen2lem1  16107  rpnnen2lem2  16108  1arithlem1  16806  vdwapval  16856  vdwlem6  16869  vdwlem8  16871  vdwlem9  16872  vdwlem10  16873  ramub1lem2  16910  ramcl  16912  sloteq  17066  prdsplusgval  17369  prdsmulrval  17371  prdsdsval  17374  prdsvscaval  17375  ismon  17630  fucco  17865  curf1  18128  curf2  18132  yonedalem4a  18178  smndex1gbas  18726  smndex1gid  18727  grplactfval  18862  galactghm  19200  pmtrval  19247  sylow1  19399  sylow2b  19419  sylow3lem5  19427  sylow3  19429  iscyg  19670  gsumzaddlem  19712  gsumzmhm  19728  ablfac2  19882  gsumdixp  20047  zncyg  20992  phllmhm  21073  isphld  21095  frlmgsum  21215  frlmipval  21222  frlmphl  21224  uvcval  21228  fczpsrbag  21362  psrmulfval  21390  mvrval  21427  subrgmvr  21471  mplcoe1  21475  mplcoe3  21476  mplcoe5  21478  mplmon2  21506  subrgascl  21511  evlslem2  21526  evlslem3  21527  evlslem1  21529  mpfrcl  21532  evlsval  21533  evlsvar  21537  mpfind  21554  selvfval  21564  selvval  21565  mhpfval  21566  coe1fval  21613  pf1ind  21758  evl1gsumadd  21761  mamuval  21772  mamufv  21773  matgsum  21823  madetsumid  21847  mat1dimmul  21862  mvmulval  21929  mvmulfv  21930  mavmulfv  21932  1mavmul  21934  marepvval0  21952  mulmarep1gsum1  21959  mdetleib  21973  mdetleib2  21974  mdetfval1  21976  mdetleib1  21977  mdet0pr  21978  m1detdiag  21983  mdetralt  21994  mdetunilem9  22006  m2detleib  22017  smadiadetlem3  22054  mat2pmatmul  22117  decpmatmul  22158  decpmatmulsumfsupp  22159  pmatcollpw1  22162  monmatcollpw  22165  pmatcollpw3lem  22169  pmatcollpw3fi1lem2  22173  pm2mpval  22181  pm2mpfval  22182  mply1topmatval  22190  mp2pm2mplem1  22192  mp2pm2mplem3  22194  ptbasfi  22969  ptcnplem  23009  ptrescn  23027  cnmpt2k  23076  xkohmeo  23203  fmval  23331  fmf  23333  ptcmpg  23445  tmdmulg  23480  prdstmdd  23512  tsmspropd  23520  prdsxmslem2  23922  metdsval  24247  fsumcn  24270  expcn  24272  lebnumlem3  24363  pcoval  24411  pi1xfrcnv  24457  cphsscph  24652  rrxds  24794  rrxmval  24806  itg11  25092  mbfi1fseqlem2  25118  mbfi1fseqlem6  25122  mbfi1fseq  25123  mbfi1flimlem  25124  mbfmullem  25127  itg2const  25142  itg2mulc  25149  itg2monolem1  25152  itg2i1fseqle  25156  itg2i1fseq  25157  itg2addlem  25160  itg2cnlem1  25163  itg2cn  25165  isibl  25167  isibl2  25168  iblitg  25170  itgz  25182  itgvallem  25186  itgvallem3  25187  iblcnlem1  25189  itgcnlem  25191  iblrelem  25192  iblposlem  25193  iblpos  25194  itgrevallem1  25196  itgposval  25197  iblss2  25207  itgss  25213  itgfsum  25228  iblabslem  25229  iblmulc2  25232  bddmulibl  25240  itgcn  25246  ellimc  25274  dvnfval  25323  cpnfval  25333  dvexp  25354  dvexp2  25355  dvmptfsum  25376  dvlipcn  25395  dvivthlem1  25409  dvfsumle  25422  dvfsumabs  25424  dvfsumlem2  25428  itgpowd  25451  elply2  25594  elplyr  25599  elplyd  25600  coeeu  25623  coelem  25624  coeeq  25625  plyco  25639  coe11  25651  coe1termlem  25656  dgrcolem1  25671  dvply2g  25682  elqaalem3  25718  eltayl  25756  tayl0  25758  taylthlem1  25769  taylthlem2  25770  ulmcau  25791  ulmdvlem1  25796  ulmdvlem3  25798  mtest  25800  mtestbdd  25801  pserval  25806  pserulm  25818  psercn  25822  pserdvlem2  25824  abelthlem3  25829  logtayl  26052  dvcxp1  26130  dvcncxp1  26133  logbmpt  26175  dmarea  26344  lgamgulmlem2  26416  lgamgulmlem5  26419  musum  26577  dchrptlem2  26650  dchrptlem3  26651  dchrpt  26652  lgsval  26686  lgsval4lem  26693  lgsneg  26706  lgsmod  26708  rpvmasum2  26897  padicfval  27001  ostth2  27022  ostth3  27023  ostth  27024  lmif  27790  islmib  27792  incistruhgr  28093  eucrct2eupth  29252  htthlem  29922  htth  29923  pjhfval  30401  hosmval  30740  hommval  30741  hodmval  30742  hfsmval  30743  hfmmval  30744  brafval  30948  kbfval  30957  mptprop  31680  psgnfzto1st  32024  linds2eq  32241  elrspunidl  32279  lbsdiflsp0  32408  fedgmullem1  32411  fedgmullem2  32412  fedgmul  32413  mdetpmtr1  32493  zar0ring  32548  ordtcnvNEW  32590  ordtrest2NEW  32593  xrhval  32688  indval  32701  esum2dlem  32780  ofceq  32785  itgeq12dv  33015  ballotlemfval  33178  vtsval  33339  lpadval  33378  ptpconn  33914  cvmliftlem15  33979  cvmlift2lem4  33987  cvmlift2  33997  snmlval  34012  snmlflim  34013  satf  34034  mrsubfval  34189  mrsubrn  34194  elmsubrn  34209  msubrn  34210  msubco  34212  faclim  34405  faclim2  34407  knoppcnlem1  35032  knoppcnlem6  35037  knoppcnlem7  35038  bj-evaleq  35616  csbrdgg  35873  curfv  36131  matunitlindflem2  36148  poimirlem5  36156  poimirlem6  36157  poimirlem7  36158  poimirlem8  36159  poimirlem10  36161  poimirlem11  36162  poimirlem12  36163  poimirlem15  36166  poimirlem16  36167  poimirlem17  36168  poimirlem18  36169  poimirlem19  36170  poimirlem20  36171  poimirlem21  36172  poimirlem22  36173  poimirlem27  36178  voliunnfl  36195  itg2addnclem  36202  itg2addnclem3  36204  itg2addnc  36205  itg2gt0cn  36206  iblabsnclem  36214  iblmulc2nc  36216  ftc1anclem2  36225  ftc1anclem6  36229  ftc1anclem8  36231  ftc1anc  36232  ftc2nc  36233  upixp  36261  rrncmslem  36364  ismrer1  36370  tendoplcbv  39311  tendopl  39312  tendoicbv  39329  tendoi  39330  dihfval  39767  lcfl7N  40037  lcfrlem8  40085  lcfrlem9  40086  lcf1o  40087  hvmapval  40296  hdmap1fval  40332  hdmapffval  40362  hdmapfval  40363  hgmapffval  40421  hgmapfval  40422  lcmineqlem7  40565  lcmineqlem12  40570  rhmmpl  40799  evlsvval  40803  evlsbagval  40806  fsuppind  40823  fsuppssindlem2  40825  fsuppssind  40826  mzpclval  41106  mzpcl2  41111  mzpexpmpt  41126  mzpsubst  41129  mzpcompact2lem  41132  rmxfval  41285  rmyfval  41286  aomclem8  41446  hbtlem1  41508  hbtlem7  41510  rfovfvd  42396  fsovrfovd  42403  fsovfvd  42404  fsovcnvlem  42407  dssmapfv2d  42412  dssmapnvod  42414  ntrneibex  42467  mnringmulrvald  42629  mnringmulrcld  42630  expgrowthi  42735  expgrowth  42737  binomcxplemdvsum  42757  addrval  42868  subrval  42869  mulvval  42870  fmulcl  43942  fmuldfeqlem1  43943  fprodcnlem  43960  fprodcn  43961  fnlimfv  44024  fnlimcnv  44028  fnlimfvre  44035  fnlimfvre2  44038  fnlimf  44039  fnlimabslt  44040  liminfval  44120  limsupresxr  44127  liminfresxr  44128  liminfvalxr  44144  fprodcncf  44261  dvnmptdivc  44299  dvnxpaek  44303  dvnmul  44304  dvmptfprod  44306  dvnprodlem1  44307  dvnprodlem2  44308  dvnprodlem3  44309  dvnprod  44310  stoweidlem2  44363  stoweidlem17  44378  stoweidlem19  44380  stoweidlem20  44381  stoweidlem43  44404  stoweidlem62  44423  stoweid  44424  dirkercncflem2  44465  fourierdlem112  44579  fourierdlem113  44580  etransclem1  44596  etransclem5  44600  etransclem17  44612  etransclem19  44614  etransclem22  44617  sge0val  44727  ovnlecvr  44919  ovncvrrp  44925  ovn0lem  44926  ovnsubaddlem1  44931  ovnsubadd  44933  hsphoif  44937  hsphoival  44940  hoidmv1lelem1  44952  hoidmv1lelem2  44953  hoidmv1lelem3  44954  hoidmv1le  44955  hoidmvlelem1  44956  hoidmvlelem2  44957  hoidmvlelem3  44958  hoidmvlelem4  44959  hoidmvlelem5  44960  hoidmvle  44961  ovnhoilem1  44962  ovnhoi  44964  hoidifhspval  44969  ovncvr2  44972  hoidifhspval2  44976  hspmbllem2  44988  hspmbllem3  44989  hspmbl  44990  ovnovollem1  45017  vonioolem2  45042  vonioo  45043  vonicclem2  45045  vonicc  45046  smflimlem4  45135  smflim  45138  smflim2  45167  smfsuplem2  45173  smfsup  45175  smfinf  45179  smflimsuplem2  45182  smflimsuplem5  45185  smflimsuplem7  45187  smflimsup  45189  cfsetsnfsetfo  45414  c0rhm  46330  c0rnghm  46331  lincop  46609  1arymaptfv  46846  itcoval  46867  itcovalpc  46878  itcovalt2  46883  ackvalsuc1mpt  46884  ackval1  46887  aacllem  47368