Theorem mpteq2dv 5215

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 5214	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))

Syntax hints:   → wi 4   = 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:  ifmpt2v  7507  ofeqd  7671  mpocurryvald  8267  rdgeq1  8423  rdgeq2  8424  omv  8522  oev  8524  oieq1  9524  oieq2  9525  cantnflem1  9701  wunex2  10750  wuncval2  10759  rpnnen1  12997  seqof2  14076  relexpsucnnr  15042  relexp1g  15043  limsupval  15488  sumeq2w  15706  sumeq2ii  15707  cbvsum  15709  cbvsumv  15710  sumeq2sdv  15717  summo  15731  fsum  15734  fsumrlim  15825  fsumo1  15826  prodeq1  15921  prodeq2w  15924  prodeq2sdv  15937  prodmo  15950  fprod  15955  bpolylem  16062  rpnnen2lem1  16230  rpnnen2lem2  16231  1arithlem1  16941  vdwapval  16991  vdwlem6  17004  vdwlem8  17006  vdwlem9  17007  vdwlem10  17008  ramub1lem2  17045  ramcl  17047  sloteq  17200  prdsplusgval  17485  prdsmulrval  17487  prdsdsval  17490  prdsvscaval  17491  ismon  17744  fucco  17976  curf1  18235  curf2  18239  yonedalem4a  18285  smndex1gbas  18878  smndex1gid  18879  grplactfval  19022  galactghm  19383  pmtrval  19430  sylow1  19582  sylow2b  19602  sylow3lem5  19610  sylow3  19612  iscyg  19858  gsumzaddlem  19900  gsumzmhm  19916  ablfac2  20070  gsumdixp  20277  c0rhm  20492  c0rnghm  20493  zncyg  21507  phllmhm  21590  isphld  21612  frlmgsum  21730  frlmipval  21737  frlmphl  21739  uvcval  21743  fczpsrbag  21879  psrmulfval  21901  psrascl  21937  mvrval  21940  subrgmvr  21989  mplcoe1  21993  mplcoe3  21994  mplcoe5  21996  mplmon2  22017  subrgascl  22022  evlslem2  22035  evlslem3  22036  evlslem1  22038  mpfrcl  22041  evlsval  22042  evlsvar  22046  mpfind  22063  selvfval  22070  selvval  22071  mhpfval  22074  psdfval  22094  psdval  22095  psdmvr  22105  coe1fval  22139  pf1ind  22291  evl1gsumadd  22294  rhmmpl  22319  rhmply1vr1  22323  mamuval  22329  mamufv  22330  matgsum  22373  madetsumid  22397  mat1dimmul  22412  mvmulval  22479  mvmulfv  22480  mavmulfv  22482  1mavmul  22484  marepvval0  22502  mulmarep1gsum1  22509  mdetleib  22523  mdetleib2  22524  mdetfval1  22526  mdetleib1  22527  mdet0pr  22528  m1detdiag  22533  mdetralt  22544  mdetunilem9  22556  m2detleib  22567  smadiadetlem3  22604  mat2pmatmul  22667  decpmatmul  22708  decpmatmulsumfsupp  22709  pmatcollpw1  22712  monmatcollpw  22715  pmatcollpw3lem  22719  pmatcollpw3fi1lem2  22723  pm2mpval  22731  pm2mpfval  22732  mply1topmatval  22740  mp2pm2mplem1  22742  mp2pm2mplem3  22744  ptbasfi  23517  ptcnplem  23557  ptrescn  23575  cnmpt2k  23624  xkohmeo  23751  fmval  23879  fmf  23881  ptcmpg  23993  tmdmulg  24028  prdstmdd  24060  tsmspropd  24068  prdsxmslem2  24466  metdsval  24785  fsumcn  24810  expcn  24812  expcnOLD  24814  lebnumlem3  24911  pcoval  24960  pi1xfrcnv  25006  cphsscph  25201  rrxds  25343  rrxmval  25355  itg11  25642  mbfi1fseqlem2  25667  mbfi1fseqlem6  25671  mbfi1fseq  25672  mbfi1flimlem  25673  mbfmullem  25676  itg2const  25691  itg2mulc  25698  itg2monolem1  25701  itg2i1fseqle  25705  itg2i1fseq  25706  itg2addlem  25709  itg2cnlem1  25712  itg2cn  25714  isibl  25716  isibl2  25717  iblitg  25719  itgeq1  25724  itgz  25732  itgvallem  25736  itgvallem3  25737  iblcnlem1  25739  itgcnlem  25741  iblrelem  25742  iblposlem  25743  iblpos  25744  itgrevallem1  25746  itgposval  25747  iblss2  25757  itgss  25763  itgfsum  25778  iblabslem  25779  iblmulc2  25782  bddmulibl  25790  itgcn  25796  ellimc  25824  dvnfval  25874  cpnfval  25884  dvexp  25907  dvexp2  25908  dvmptfsum  25929  dvlipcn  25949  dvivthlem1  25963  dvfsumle  25976  dvfsumleOLD  25977  dvfsumabs  25979  dvfsumlem2  25983  dvfsumlem2OLD  25984  itgpowd  26007  elply2  26151  elplyr  26156  elplyd  26157  coeeu  26180  coelem  26181  coeeq  26182  plyco  26196  coe11  26208  coe1termlem  26213  dgrcolem1  26229  dvply2g  26242  dvply2gOLD  26243  elqaalem3  26279  eltayl  26317  tayl0  26319  taylthlem1  26331  taylthlem2  26332  taylthlem2OLD  26333  ulmcau  26354  ulmdvlem1  26359  ulmdvlem3  26361  mtest  26363  mtestbdd  26364  pserval  26369  pserulm  26381  psercn  26386  pserdvlem2  26388  abelthlem3  26393  logtayl  26619  dvcxp1  26699  dvcncxp1  26702  logbmpt  26748  dmarea  26917  lgamgulmlem2  26990  lgamgulmlem5  26993  musum  27151  dchrptlem2  27226  dchrptlem3  27227  dchrpt  27228  lgsval  27262  lgsval4lem  27269  lgsneg  27282  lgsmod  27284  rpvmasum2  27473  padicfval  27577  ostth2  27598  ostth3  27599  ostth  27600  lmif  28710  islmib  28712  incistruhgr  29004  eucrct2eupth  30172  htthlem  30844  htth  30845  pjhfval  31323  hosmval  31662  hommval  31663  hodmval  31664  hfsmval  31665  hfmmval  31666  brafval  31870  kbfval  31879  mptprop  32621  indval  32776  psgnfzto1st  33062  elrgspnlem1  33183  elrgspnlem2  33184  elrgspnlem3  33185  elrgspnlem4  33186  elrgspn  33187  elrgspnsubrunlem1  33188  linds2eq  33342  elrspunidl  33389  elrspunsn  33390  evl1deg1  33535  evl1deg2  33536  evl1deg3  33537  lbsdiflsp0  33612  fedgmullem1  33615  fedgmullem2  33616  fedgmul  33617  evls1fldgencl  33657  fldextrspunlsplem  33660  fldextrspunlsp  33661  mdetpmtr1  33800  zar0ring  33855  ordtcnvNEW  33897  ordtrest2NEW  33900  xrhval  33995  esum2dlem  34069  ofceq  34074  itgeq12dv  34304  ballotlemfval  34468  vtsval  34615  lpadval  34654  ptpconn  35201  cvmliftlem15  35266  cvmlift2lem4  35274  cvmlift2  35284  snmlval  35299  snmlflim  35300  satf  35321  mrsubfval  35476  mrsubrn  35481  elmsubrn  35496  msubrn  35497  msubco  35499  faclim  35709  faclim2  35711  prodeq12sdv  36182  itgeq12sdv  36183  cbvsumdavw  36243  cbvproddavw  36244  cbvsumdavw2  36259  cbvproddavw2  36260  knoppcnlem1  36457  knoppcnlem6  36462  knoppcnlem7  36463  bj-evaleq  37036  csbrdgg  37293  curfv  37570  matunitlindflem2  37587  poimirlem5  37595  poimirlem6  37596  poimirlem7  37597  poimirlem8  37598  poimirlem10  37600  poimirlem11  37601  poimirlem12  37602  poimirlem15  37605  poimirlem16  37606  poimirlem17  37607  poimirlem18  37608  poimirlem19  37609  poimirlem20  37610  poimirlem21  37611  poimirlem22  37612  poimirlem27  37617  voliunnfl  37634  itg2addnclem  37641  itg2addnclem3  37643  itg2addnc  37644  itg2gt0cn  37645  iblabsnclem  37653  iblmulc2nc  37655  ftc1anclem2  37664  ftc1anclem6  37668  ftc1anclem8  37670  ftc1anc  37671  ftc2nc  37672  upixp  37699  rrncmslem  37802  ismrer1  37808  tendoplcbv  40740  tendopl  40741  tendoicbv  40758  tendoi  40759  dihfval  41196  lcfl7N  41466  lcfrlem8  41514  lcfrlem9  41515  lcf1o  41516  hvmapval  41725  hdmap1fval  41761  hdmapffval  41791  hdmapfval  41792  hgmapffval  41850  hgmapfval  41851  lcmineqlem7  41994  lcmineqlem12  41999  aks6d1c6lem5  42136  rhmpsr  42522  evlsvval  42530  evlsvvval  42533  evlsbagval  42536  selvvvval  42555  evlselv  42557  fsuppind  42560  fsuppssindlem2  42562  fsuppssind  42563  mzpclval  42695  mzpcl2  42700  mzpexpmpt  42715  mzpsubst  42718  mzpcompact2lem  42721  rmxfval  42874  rmyfval  42875  aomclem8  43032  hbtlem1  43094  hbtlem7  43096  rfovfvd  43973  fsovrfovd  43980  fsovfvd  43981  fsovcnvlem  43984  dssmapfv2d  43989  dssmapnvod  43991  ntrneibex  44044  mnringmulrvald  44199  mnringmulrcld  44200  expgrowthi  44305  expgrowth  44307  binomcxplemdvsum  44327  addrval  44438  subrval  44439  mulvval  44440  fmulcl  45558  fmuldfeqlem1  45559  fprodcnlem  45576  fprodcn  45577  fnlimfv  45640  fnlimcnv  45644  fnlimfvre  45651  fnlimfvre2  45654  fnlimf  45655  fnlimabslt  45656  liminfval  45736  limsupresxr  45743  liminfresxr  45744  liminfvalxr  45760  fprodcncf  45877  dvnmptdivc  45915  dvnxpaek  45919  dvnmul  45920  dvmptfprod  45922  dvnprodlem1  45923  dvnprodlem2  45924  dvnprodlem3  45925  dvnprod  45926  stoweidlem2  45979  stoweidlem17  45994  stoweidlem19  45996  stoweidlem20  45997  stoweidlem43  46020  stoweidlem62  46039  stoweid  46040  dirkercncflem2  46081  fourierdlem112  46195  fourierdlem113  46196  etransclem1  46212  etransclem5  46216  etransclem17  46228  etransclem19  46230  etransclem22  46233  sge0val  46343  ovnlecvr  46535  ovncvrrp  46541  ovn0lem  46542  ovnsubaddlem1  46547  ovnsubadd  46549  hsphoif  46553  hsphoival  46556  hoidmv1lelem1  46568  hoidmv1lelem2  46569  hoidmv1lelem3  46570  hoidmv1le  46571  hoidmvlelem1  46572  hoidmvlelem2  46573  hoidmvlelem3  46574  hoidmvlelem4  46575  hoidmvlelem5  46576  hoidmvle  46577  ovnhoilem1  46578  ovnhoi  46580  hoidifhspval  46585  ovncvr2  46588  hoidifhspval2  46592  hspmbllem2  46604  hspmbllem3  46605  hspmbl  46606  ovnovollem1  46633  vonioolem2  46658  vonioo  46659  vonicclem2  46661  vonicc  46662  smflimlem4  46751  smflim  46754  smflim2  46783  smfsuplem2  46789  smfsup  46791  smfinf  46795  smflimsuplem2  46798  smflimsuplem5  46801  smflimsuplem7  46803  smflimsup  46805  cfsetsnfsetfo  47037  lincop  48332  1arymaptfv  48568  itcoval  48589  itcovalpc  48600  itcovalt2  48605  ackvalsuc1mpt  48606  ackval1  48609  fuco21  49195  prcofval  49237  aacllem  49613