Theorem mpteq2dv 5207

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2146   ↦ cmpt 5194

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 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-opab 5176  df-mpt 5195

This theorem is used by:  ifmpt2v  7518  ofeqd  7682  mpocurryvald  8268  rdgeq1  8400  rdgeq2  8401  omv  8499  oev  8501  oieq1  9477  oieq2  9478  cantnflem1  9661  wunex2  10734  wuncval2  10743  indval  12232  rpnnen1  13019  seqof2  14110  relexpsucnnr  15082  relexp1g  15083  limsupval  15545  sumeq2w  15763  sumeq2ii  15764  cbvsum  15766  cbvsumv  15767  sumeq2sdv  15774  summo  15787  fsum  15790  fsumrlim  15882  fsumo1  15883  prodeq1  15980  prodeq2w  15983  prodeq2sdv  15996  prodmo  16009  fprod  16014  bpolylem  16120  rpnnen2lem1  16288  rpnnen2lem2  16289  1arithlem1  17001  vdwapval  17051  vdwlem6  17064  vdwlem8  17066  vdwlem9  17067  vdwlem10  17068  ramub1lem2  17105  ramcl  17107  sloteq  17261  prdsplusgval  17544  prdsmulrval  17546  prdsdsval  17549  prdsvscaval  17550  ismon  17808  fucco  18040  curf1  18299  curf2  18303  yonedalem4a  18349  smndex1gbas  18985  smndex1gbasOLD  18986  smndex1gid  18987  smndex1gidOLD  18988  smndex1igid  18989  grplactfval  19131  galactghm  19498  pmtrval  19545  sylow1  19697  sylow2b  19717  sylow3lem5  19725  sylow3  19727  iscyg  19973  gsumzaddlem  20015  gsumzmhm  20031  ablfac2  20185  gsumdixp  20426  c0rhm  20663  c0rnghm  20664  zncyg  21728  phllmhm  21812  isphld  21834  frlmgsum  21952  frlmipval  21959  frlmphl  21961  uvcval  21965  fczpsrbag  22101  psrmulfval  22123  psrascl  22158  mvrval  22161  subrgmvr  22214  mplcoe1  22218  mplcoe3  22219  mplcoe5  22221  mplmon2  22242  subrgascl  22247  evlslem2  22260  evlslem3  22261  evlslem1  22263  mpfrcl  22266  evlsval  22267  evlsvval  22271  evlsvvval  22274  evlsvar  22276  mpfind  22296  selvfval  22300  selvval  22301  selvvvval  22323  mhpfval  22331  psdfval  22351  psdval  22352  psdmvr  22362  coe1fval  22395  pf1ind  22545  evl1gsumadd  22548  rhmmpl  22570  rhmply1vr1  22574  mamuval  22580  mamufv  22581  matgsum  22624  madetsumid  22648  mat1dimmul  22663  mvmulval  22730  mvmulfv  22731  mavmulfv  22733  1mavmul  22735  marepvval0  22753  mulmarep1gsum1  22760  mdetleib  22774  mdetleib2  22775  mdetfval1  22777  mdetleib1  22778  mdet0pr  22779  m1detdiag  22784  mdetralt  22795  mdetunilem9  22807  m2detleib  22818  smadiadetlem3  22855  mat2pmatmul  22918  decpmatmul  22959  decpmatmulsumfsupp  22960  pmatcollpw1  22963  monmatcollpw  22966  pmatcollpw3lem  22970  pmatcollpw3fi1lem2  22974  pm2mpval  22982  pm2mpfval  22983  mply1topmatval  22991  mp2pm2mplem1  22993  mp2pm2mplem3  22995  ptbasfi  23769  ptcnplem  23809  ptrescn  23827  cnmpt2k  23876  xkohmeo  24003  fmval  24131  fmf  24133  ptcmpg  24245  tmdmulg  24280  prdstmdd  24312  tsmspropd  24320  prdsxmslem2  24717  metdsval  25036  fsumcn  25060  expcn  25062  lebnumlem3  25153  pcoval  25201  pi1xfrcnv  25247  cphsscph  25441  rrxds  25583  rrxmval  25595  itg11  25881  mbfi1fseqlem2  25906  mbfi1fseqlem6  25910  mbfi1fseq  25911  mbfi1flimlem  25912  mbfmullem  25915  itg2const  25930  itg2mulc  25937  itg2monolem1  25940  itg2i1fseqle  25944  itg2i1fseq  25945  itg2addlem  25948  itg2cnlem1  25951  itg2cn  25953  isibl  25955  isibl2  25956  iblitg  25958  itgeq1  25963  itgz  25971  itgvallem  25975  itgvallem3  25976  iblcnlem1  25978  itgcnlem  25980  iblrelem  25981  iblposlem  25982  iblpos  25983  itgrevallem1  25985  itgposval  25986  iblss2  25996  itgss  26002  itgfsum  26017  iblabslem  26018  iblmulc2  26021  bddmulibl  26029  itgcn  26035  ellimc  26063  dvnfval  26112  cpnfval  26122  dvexp  26143  dvexp2  26144  dvmptfsum  26165  dvlipcn  26184  dvivthlem1  26198  dvfsumle  26211  dvfsumabs  26213  dvfsumlem2  26217  itgpowd  26240  elply2  26384  elplyr  26389  elplyd  26390  coeeu  26413  coelem  26414  coeeq  26415  plyco  26429  coe11  26441  coe1termlem  26446  dgrcolem1  26461  dvply2g  26477  elqaalem3  26513  eltayl  26554  tayl0  26556  taylthlem1  26567  taylthlem2  26568  ulmcau  26589  ulmdvlem1  26594  ulmdvlem3  26596  mtest  26598  mtestbdd  26599  pserval  26604  pserulm  26616  psercn  26620  pserdvlem2  26622  abelthlem3  26627  logtayl  26856  dvcxp1  26936  dvcncxp1  26939  logbmpt  26984  dmarea  27153  lgamgulmlem2  27225  lgamgulmlem5  27228  musum  27386  dchrptlem2  27460  dchrptlem3  27461  dchrpt  27462  lgsval  27496  lgsval4lem  27503  lgsneg  27516  lgsmod  27518  rpvmasum2  27707  padicfval  27811  ostth2  27832  ostth3  27833  ostth  27834  lmif  29125  islmib  29127  incistruhgr  29460  eucrct2eupth  30643  htthlem  31316  htth  31317  pjhfval  31795  hosmval  32134  hommval  32135  hodmval  32136  hfsmval  32137  hfmmval  32138  brafval  32342  kbfval  32351  mptprop  33090  indsn  33229  psgnfzto1st  33465  fxpsubm  33532  fxpsubg  33533  fxpsubrg  33534  elrgspnlem1  33602  elrgspnlem2  33603  elrgspnlem3  33604  elrgspnlem4  33605  elrgspn  33606  elrgspnsubrunlem1  33607  linds2eq  33734  elrspunidl  33776  elrspunsn  33777  evl1deg1  33906  evl1deg2  33907  evl1deg3  33908  mplasclco  33946  selvply1rhmlema  33948  selvply1rhmlemb  33949  selvply1rhmlem2  33951  selvply1rhmlem3  33952  selvply1rhmlem4  33953  selvply1rhmlem5  33954  selvply1rhm  33955  mplidom  33958  extvfval  33962  extvfv  33963  mvrvalind  33968  evlextv  33972  mplvrpmfgalem  33974  mplvrpmga  33975  mplvrpmmhm  33976  mplvrpmrhm  33977  psrgsum  33978  psrmonmul2  33981  psrmonprod  33982  splysubrg  33990  issply  33991  esplyval  33992  esplyfvaln  34004  vietalem  34009  vieta  34010  lbsdiflsp0  34056  fedgmullem1  34059  fedgmullem2  34060  fedgmul  34061  evls1fldgencl  34100  fldextrspunlsplem  34103  fldextrspunlsp  34104  extdgfialglem2  34123  mdetpmtr1  34253  zar0ring  34308  ordtcnvNEW  34350  ordtrest2NEW  34353  xrhval  34448  esum2dlem  34522  ofceq  34527  itgeq12dv  34757  ballotlemfval  34921  vtsval  35065  lpadval  35107  ptpconn  35738  cvmliftlem15  35803  cvmlift2lem4  35811  cvmlift2  35821  snmlval  35836  snmlflim  35837  satf  35858  mrsubfval  36013  mrsubrn  36018  elmsubrn  36033  msubrn  36034  msubco  36036  faclim  36251  faclim2  36253  prodeq12sdv  36763  itgeq12sdv  36764  cbvsumdavw  36824  cbvproddavw  36825  cbvsumdavw2  36840  cbvproddavw2  36841  knoppcnlem1  37115  knoppcnlem6  37120  knoppcnlem7  37121  bj-evaleq  37746  csbrdgg  38008  curfv  38284  matunitlindflem2  38301  poimirlem5  38309  poimirlem6  38310  poimirlem7  38311  poimirlem8  38312  poimirlem10  38314  poimirlem11  38315  poimirlem12  38316  poimirlem15  38319  poimirlem16  38320  poimirlem17  38321  poimirlem18  38322  poimirlem19  38323  poimirlem20  38324  poimirlem21  38325  poimirlem22  38326  poimirlem27  38331  voliunnfl  38348  itg2addnclem  38355  itg2addnclem3  38357  itg2addnc  38358  itg2gt0cn  38359  iblabsnclem  38367  iblmulc2nc  38369  ftc1anclem2  38378  ftc1anclem6  38382  ftc1anclem8  38384  ftc1anc  38385  ftc2nc  38386  upixp  38413  rrncmslem  38516  ismrer1  38522  tendoplcbv  41582  tendopl  41583  tendoicbv  41600  tendoi  41601  dihfval  42038  lcfl7N  42308  lcfrlem8  42356  lcfrlem9  42357  lcf1o  42358  hvmapval  42567  hdmap1fval  42603  hdmapffval  42633  hdmapfval  42634  hgmapffval  42692  hgmapfval  42693  lcmineqlem7  42835  lcmineqlem12  42840  aks6d1c6lem5  42977  rhmpsr  43348  evlsbagval  43351  evlselv  43354  fsuppind  43355  fsuppssindlem2  43357  fsuppssind  43358  mzpclval  43489  mzpcl2  43494  mzpexpmpt  43509  mzpsubst  43512  mzpcompact2lem  43515  rmxfval  43664  rmyfval  43665  aomclem8  43821  hbtlem1  43883  hbtlem7  43885  rfovfvd  44761  fsovrfovd  44768  fsovfvd  44769  fsovcnvlem  44772  dssmapfv2d  44777  dssmapnvod  44779  ntrneibex  44832  mnringmulrvald  44984  mnringmulrcld  44985  expgrowthi  45076  expgrowth  45078  binomcxplemdvsum  45098  addrval  45207  subrval  45208  mulvval  45209  fmulcl  46330  fmuldfeqlem1  46331  fprodcnlem  46348  fprodcn  46349  fnlimfv  46410  fnlimcnv  46414  fnlimfvre  46421  fnlimfvre2  46424  fnlimf  46425  fnlimabslt  46426  liminfval  46506  limsupresxr  46513  liminfresxr  46514  liminfvalxr  46530  fprodcncf  46647  dvnmptdivc  46685  dvnxpaek  46689  dvnmul  46690  dvmptfprod  46692  dvnprodlem1  46693  dvnprodlem2  46694  dvnprodlem3  46695  dvnprod  46696  stoweidlem2  46749  stoweidlem17  46764  stoweidlem19  46766  stoweidlem20  46767  stoweidlem43  46790  stoweidlem62  46809  stoweid  46810  dirkercncflem2  46851  fourierdlem112  46965  fourierdlem113  46966  etransclem1  46982  etransclem5  46986  etransclem17  46998  etransclem19  47000  etransclem22  47003  sge0val  47113  ovnlecvr  47305  ovncvrrp  47311  ovn0lem  47312  ovnsubaddlem1  47317  ovnsubadd  47319  hsphoif  47323  hsphoival  47326  hoidmv1lelem1  47338  hoidmv1lelem2  47339  hoidmv1lelem3  47340  hoidmv1le  47341  hoidmvlelem1  47342  hoidmvlelem2  47343  hoidmvlelem3  47344  hoidmvlelem4  47345  hoidmvlelem5  47346  hoidmvle  47347  ovnhoilem1  47348  ovnhoi  47350  hoidifhspval  47355  ovncvr2  47358  hoidifhspval2  47362  hspmbllem2  47374  hspmbllem3  47375  hspmbl  47376  ovnovollem1  47403  vonioolem2  47428  vonioo  47429  vonicclem2  47431  vonicc  47432  smflimlem4  47521  smflim  47524  smflim2  47553  smfsuplem2  47559  smfsup  47561  smfinf  47565  smflimsuplem2  47568  smflimsuplem5  47571  smflimsuplem7  47573  smflimsup  47575  cfsetsnfsetfo  47830  lincop  49221  1arymaptfv  49453  itcoval  49474  itcovalpc  49485  itcovalt2  49490  ackvalsuc1mpt  49491  ackval1  49494  fuco21  50147  prcofval  50189  aacllem  50654  crosspval  50669  crosspdot0i  50678