Theorem mpteq2dv 5201

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 480	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)
3	2	mpteq2dva 5200	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109   ↦ cmpt 5188

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-opab 5170  df-mpt 5189

This theorem is referenced by:  ifmpt2v  7491  ofeqd  7655  mpocurryvald  8249  rdgeq1  8379  rdgeq2  8380  omv  8476  oev  8478  oieq1  9465  oieq2  9466  cantnflem1  9642  wunex2  10691  wuncval2  10700  rpnnen1  12942  seqof2  14025  relexpsucnnr  14991  relexp1g  14992  limsupval  15440  sumeq2w  15658  sumeq2ii  15659  cbvsum  15661  cbvsumv  15662  sumeq2sdv  15669  summo  15683  fsum  15686  fsumrlim  15777  fsumo1  15778  prodeq1  15873  prodeq2w  15876  prodeq2sdv  15889  prodmo  15902  fprod  15907  bpolylem  16014  rpnnen2lem1  16182  rpnnen2lem2  16183  1arithlem1  16894  vdwapval  16944  vdwlem6  16957  vdwlem8  16959  vdwlem9  16960  vdwlem10  16961  ramub1lem2  16998  ramcl  17000  sloteq  17153  prdsplusgval  17436  prdsmulrval  17438  prdsdsval  17441  prdsvscaval  17442  ismon  17695  fucco  17927  curf1  18186  curf2  18190  yonedalem4a  18236  smndex1gbas  18829  smndex1gid  18830  grplactfval  18973  galactghm  19334  pmtrval  19381  sylow1  19533  sylow2b  19553  sylow3lem5  19561  sylow3  19563  iscyg  19809  gsumzaddlem  19851  gsumzmhm  19867  ablfac2  20021  gsumdixp  20228  c0rhm  20443  c0rnghm  20444  zncyg  21458  phllmhm  21541  isphld  21563  frlmgsum  21681  frlmipval  21688  frlmphl  21690  uvcval  21694  fczpsrbag  21830  psrmulfval  21852  psrascl  21888  mvrval  21891  subrgmvr  21940  mplcoe1  21944  mplcoe3  21945  mplcoe5  21947  mplmon2  21968  subrgascl  21973  evlslem2  21986  evlslem3  21987  evlslem1  21989  mpfrcl  21992  evlsval  21993  evlsvar  21997  mpfind  22014  selvfval  22021  selvval  22022  mhpfval  22025  psdfval  22045  psdval  22046  psdmvr  22056  coe1fval  22090  pf1ind  22242  evl1gsumadd  22245  rhmmpl  22270  rhmply1vr1  22274  mamuval  22280  mamufv  22281  matgsum  22324  madetsumid  22348  mat1dimmul  22363  mvmulval  22430  mvmulfv  22431  mavmulfv  22433  1mavmul  22435  marepvval0  22453  mulmarep1gsum1  22460  mdetleib  22474  mdetleib2  22475  mdetfval1  22477  mdetleib1  22478  mdet0pr  22479  m1detdiag  22484  mdetralt  22495  mdetunilem9  22507  m2detleib  22518  smadiadetlem3  22555  mat2pmatmul  22618  decpmatmul  22659  decpmatmulsumfsupp  22660  pmatcollpw1  22663  monmatcollpw  22666  pmatcollpw3lem  22670  pmatcollpw3fi1lem2  22674  pm2mpval  22682  pm2mpfval  22683  mply1topmatval  22691  mp2pm2mplem1  22693  mp2pm2mplem3  22695  ptbasfi  23468  ptcnplem  23508  ptrescn  23526  cnmpt2k  23575  xkohmeo  23702  fmval  23830  fmf  23832  ptcmpg  23944  tmdmulg  23979  prdstmdd  24011  tsmspropd  24019  prdsxmslem2  24417  metdsval  24736  fsumcn  24761  expcn  24763  expcnOLD  24765  lebnumlem3  24862  pcoval  24911  pi1xfrcnv  24957  cphsscph  25151  rrxds  25293  rrxmval  25305  itg11  25592  mbfi1fseqlem2  25617  mbfi1fseqlem6  25621  mbfi1fseq  25622  mbfi1flimlem  25623  mbfmullem  25626  itg2const  25641  itg2mulc  25648  itg2monolem1  25651  itg2i1fseqle  25655  itg2i1fseq  25656  itg2addlem  25659  itg2cnlem1  25662  itg2cn  25664  isibl  25666  isibl2  25667  iblitg  25669  itgeq1  25674  itgz  25682  itgvallem  25686  itgvallem3  25687  iblcnlem1  25689  itgcnlem  25691  iblrelem  25692  iblposlem  25693  iblpos  25694  itgrevallem1  25696  itgposval  25697  iblss2  25707  itgss  25713  itgfsum  25728  iblabslem  25729  iblmulc2  25732  bddmulibl  25740  itgcn  25746  ellimc  25774  dvnfval  25824  cpnfval  25834  dvexp  25857  dvexp2  25858  dvmptfsum  25879  dvlipcn  25899  dvivthlem1  25913  dvfsumle  25926  dvfsumleOLD  25927  dvfsumabs  25929  dvfsumlem2  25933  dvfsumlem2OLD  25934  itgpowd  25957  elply2  26101  elplyr  26106  elplyd  26107  coeeu  26130  coelem  26131  coeeq  26132  plyco  26146  coe11  26158  coe1termlem  26163  dgrcolem1  26179  dvply2g  26192  dvply2gOLD  26193  elqaalem3  26229  eltayl  26267  tayl0  26269  taylthlem1  26281  taylthlem2  26282  taylthlem2OLD  26283  ulmcau  26304  ulmdvlem1  26309  ulmdvlem3  26311  mtest  26313  mtestbdd  26314  pserval  26319  pserulm  26331  psercn  26336  pserdvlem2  26338  abelthlem3  26343  logtayl  26569  dvcxp1  26649  dvcncxp1  26652  logbmpt  26698  dmarea  26867  lgamgulmlem2  26940  lgamgulmlem5  26943  musum  27101  dchrptlem2  27176  dchrptlem3  27177  dchrpt  27178  lgsval  27212  lgsval4lem  27219  lgsneg  27232  lgsmod  27234  rpvmasum2  27423  padicfval  27527  ostth2  27548  ostth3  27549  ostth  27550  lmif  28712  islmib  28714  incistruhgr  29006  eucrct2eupth  30174  htthlem  30846  htth  30847  pjhfval  31325  hosmval  31664  hommval  31665  hodmval  31666  hfsmval  31667  hfmmval  31668  brafval  31872  kbfval  31881  mptprop  32621  indval  32776  psgnfzto1st  33062  fxpsubm  33129  elrgspnlem1  33193  elrgspnlem2  33194  elrgspnlem3  33195  elrgspnlem4  33196  elrgspn  33197  elrgspnsubrunlem1  33198  linds2eq  33352  elrspunidl  33399  elrspunsn  33400  evl1deg1  33545  evl1deg2  33546  evl1deg3  33547  lbsdiflsp0  33622  fedgmullem1  33625  fedgmullem2  33626  fedgmul  33627  evls1fldgencl  33665  fldextrspunlsplem  33668  fldextrspunlsp  33669  mdetpmtr1  33813  zar0ring  33868  ordtcnvNEW  33910  ordtrest2NEW  33913  xrhval  34008  esum2dlem  34082  ofceq  34087  itgeq12dv  34317  ballotlemfval  34481  vtsval  34628  lpadval  34667  ptpconn  35220  cvmliftlem15  35285  cvmlift2lem4  35293  cvmlift2  35303  snmlval  35318  snmlflim  35319  satf  35340  mrsubfval  35495  mrsubrn  35500  elmsubrn  35515  msubrn  35516  msubco  35518  faclim  35733  faclim2  35735  prodeq12sdv  36206  itgeq12sdv  36207  cbvsumdavw  36267  cbvproddavw  36268  cbvsumdavw2  36283  cbvproddavw2  36284  knoppcnlem1  36481  knoppcnlem6  36486  knoppcnlem7  36487  bj-evaleq  37060  csbrdgg  37317  curfv  37594  matunitlindflem2  37611  poimirlem5  37619  poimirlem6  37620  poimirlem7  37621  poimirlem8  37622  poimirlem10  37624  poimirlem11  37625  poimirlem12  37626  poimirlem15  37629  poimirlem16  37630  poimirlem17  37631  poimirlem18  37632  poimirlem19  37633  poimirlem20  37634  poimirlem21  37635  poimirlem22  37636  poimirlem27  37641  voliunnfl  37658  itg2addnclem  37665  itg2addnclem3  37667  itg2addnc  37668  itg2gt0cn  37669  iblabsnclem  37677  iblmulc2nc  37679  ftc1anclem2  37688  ftc1anclem6  37692  ftc1anclem8  37694  ftc1anc  37695  ftc2nc  37696  upixp  37723  rrncmslem  37826  ismrer1  37832  tendoplcbv  40769  tendopl  40770  tendoicbv  40787  tendoi  40788  dihfval  41225  lcfl7N  41495  lcfrlem8  41543  lcfrlem9  41544  lcf1o  41545  hvmapval  41754  hdmap1fval  41790  hdmapffval  41820  hdmapfval  41821  hgmapffval  41879  hgmapfval  41880  lcmineqlem7  42023  lcmineqlem12  42028  aks6d1c6lem5  42165  rhmpsr  42540  evlsvval  42548  evlsvvval  42551  evlsbagval  42554  selvvvval  42573  evlselv  42575  fsuppind  42578  fsuppssindlem2  42580  fsuppssind  42581  mzpclval  42713  mzpcl2  42718  mzpexpmpt  42733  mzpsubst  42736  mzpcompact2lem  42739  rmxfval  42892  rmyfval  42893  aomclem8  43050  hbtlem1  43112  hbtlem7  43114  rfovfvd  43991  fsovrfovd  43998  fsovfvd  43999  fsovcnvlem  44002  dssmapfv2d  44007  dssmapnvod  44009  ntrneibex  44062  mnringmulrvald  44216  mnringmulrcld  44217  expgrowthi  44322  expgrowth  44324  binomcxplemdvsum  44344  addrval  44455  subrval  44456  mulvval  44457  fmulcl  45579  fmuldfeqlem1  45580  fprodcnlem  45597  fprodcn  45598  fnlimfv  45661  fnlimcnv  45665  fnlimfvre  45672  fnlimfvre2  45675  fnlimf  45676  fnlimabslt  45677  liminfval  45757  limsupresxr  45764  liminfresxr  45765  liminfvalxr  45781  fprodcncf  45898  dvnmptdivc  45936  dvnxpaek  45940  dvnmul  45941  dvmptfprod  45943  dvnprodlem1  45944  dvnprodlem2  45945  dvnprodlem3  45946  dvnprod  45947  stoweidlem2  46000  stoweidlem17  46015  stoweidlem19  46017  stoweidlem20  46018  stoweidlem43  46041  stoweidlem62  46060  stoweid  46061  dirkercncflem2  46102  fourierdlem112  46216  fourierdlem113  46217  etransclem1  46233  etransclem5  46237  etransclem17  46249  etransclem19  46251  etransclem22  46254  sge0val  46364  ovnlecvr  46556  ovncvrrp  46562  ovn0lem  46563  ovnsubaddlem1  46568  ovnsubadd  46570  hsphoif  46574  hsphoival  46577  hoidmv1lelem1  46589  hoidmv1lelem2  46590  hoidmv1lelem3  46591  hoidmv1le  46592  hoidmvlelem1  46593  hoidmvlelem2  46594  hoidmvlelem3  46595  hoidmvlelem4  46596  hoidmvlelem5  46597  hoidmvle  46598  ovnhoilem1  46599  ovnhoi  46601  hoidifhspval  46606  ovncvr2  46609  hoidifhspval2  46613  hspmbllem2  46625  hspmbllem3  46626  hspmbl  46627  ovnovollem1  46654  vonioolem2  46679  vonioo  46680  vonicclem2  46682  vonicc  46683  smflimlem4  46772  smflim  46775  smflim2  46804  smfsuplem2  46810  smfsup  46812  smfinf  46816  smflimsuplem2  46819  smflimsuplem5  46822  smflimsuplem7  46824  smflimsup  46826  cfsetsnfsetfo  47061  lincop  48397  1arymaptfv  48629  itcoval  48650  itcovalpc  48661  itcovalt2  48666  ackvalsuc1mpt  48667  ackval1  48670  fuco21  49325  prcofval  49367  aacllem  49790