Theorem mpteq2dv 4932

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

Syntax hints:   → wi 4   = wceq 1637   ∈ wcel 2155   ↦ cmpt 4916

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2067  ax-7 2103  ax-9 2164  ax-10 2184  ax-11 2200  ax-12 2213  ax-ext 2781

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2060  df-clab 2789  df-cleq 2795  df-clel 2798  df-ral 3097  df-opab 4900  df-mpt 4917

This theorem is referenced by:  ofeq  7123  mpt2curryvald  7625  rdgeq1  7737  rdgeq2  7738  omv  7823  oev  7825  oieq1  8650  oieq2  8651  cantnflem1  8827  wunex2  9839  wuncval2  9848  rpnnen1  12033  seqof2  13076  relexpsucnnr  13982  relexp1g  13983  limsupval  14422  sumeq2w  14639  sumeq2ii  14640  cbvsum  14642  summo  14665  fsum  14668  fsumrlim  14759  fsumo1  14760  prodeq2w  14857  prodmo  14881  fprod  14886  bpolylem  14993  rpnnen2lem1  15157  rpnnen2lem2  15158  1arithlem1  15838  vdwapval  15888  vdwlem6  15901  vdwlem8  15903  vdwlem9  15904  vdwlem10  15905  ramub1lem2  15942  ramcl  15944  sloteq  16067  prdsplusgval  16332  prdsmulrval  16334  prdsdsval  16337  prdsvscaval  16338  ismon  16591  fucco  16820  curf1  17064  curf2  17068  yonedalem4a  17114  grplactfval  17715  galactghm  18018  pmtrval  18066  sylow1  18213  sylow2b  18233  sylow3lem5  18241  sylow3  18243  iscyg  18476  gsumzaddlem  18516  gsumzmhm  18532  ablfac2  18684  gsumdixp  18805  fczpsrbag  19570  psrmulfval  19588  mvrval  19624  subrgmvr  19664  mplcoe1  19668  mplcoe3  19669  mplcoe5  19671  mplmon2  19695  subrgascl  19700  evlslem2  19714  evlslem3  19716  evlslem1  19717  mpfrcl  19720  evlsval  19721  evlsvar  19725  mpfind  19738  coe1fval  19777  pf1ind  19921  evl1gsumadd  19924  zncyg  20098  phllmhm  20181  isphld  20203  frlmgsum  20315  frlmipval  20322  frlmphl  20324  uvcval  20328  mamuval  20396  mamufv  20397  matgsum  20447  madetsumid  20472  mat1dimmul  20487  mvmulval  20554  mvmulfv  20555  mavmulfv  20557  1mavmul  20559  marepvval0  20577  mulmarep1gsum1  20584  mdetleib  20598  mdetleib2  20599  mdetfval1  20601  mdetleib1  20602  mdet0pr  20603  m1detdiag  20608  mdetralt  20619  mdetunilem9  20631  m2detleib  20642  smadiadetlem3  20680  mat2pmatmul  20743  decpmatmul  20784  decpmatmulsumfsupp  20785  pmatcollpw1  20788  monmatcollpw  20791  pmatcollpw3lem  20795  pmatcollpw3fi1lem2  20799  pm2mpval  20807  pm2mpfval  20808  mply1topmatval  20816  mp2pm2mplem1  20818  mp2pm2mplem3  20820  ptbasfi  21592  ptcnplem  21632  ptrescn  21650  cnmpt2k  21699  xkohmeo  21826  fmval  21954  fmf  21956  ptcmpg  22068  tmdmulg  22103  prdstmdd  22134  tsmspropd  22142  prdsxmslem2  22541  metdsval  22857  fsumcn  22880  expcn  22882  lebnumlem3  22969  pcoval  23017  pi1xfrcnv  23063  rrxds  23387  rrxmval  23394  itg11  23666  mbfi1fseqlem2  23691  mbfi1fseqlem6  23695  mbfi1fseq  23696  mbfi1flimlem  23697  mbfmullem  23700  itg2const  23715  itg2mulc  23722  itg2monolem1  23725  itg2i1fseqle  23729  itg2i1fseq  23730  itg2addlem  23733  itg2cnlem1  23736  itg2cn  23738  isibl  23740  isibl2  23741  iblitg  23743  itgz  23755  itgvallem  23759  itgvallem3  23760  iblcnlem1  23762  itgcnlem  23764  iblrelem  23765  iblposlem  23766  iblpos  23767  itgrevallem1  23769  itgposval  23770  iblss2  23780  itgss  23786  itgfsum  23801  iblabslem  23802  iblmulc2  23805  bddmulibl  23813  itgcn  23817  ellimc  23845  dvnfval  23893  cpnfval  23903  dvexp  23924  dvexp2  23925  dvmptfsum  23946  dvlipcn  23965  dvivthlem1  23979  dvfsumle  23992  dvfsumabs  23994  dvfsumlem2  23998  elply2  24160  elplyr  24165  elplyd  24166  coeeu  24189  coelem  24190  coeeq  24191  plyco  24205  coe11  24217  coe1termlem  24222  dgrcolem1  24237  dvply2g  24248  elqaalem3  24284  eltayl  24322  tayl0  24324  taylthlem1  24335  taylthlem2  24336  ulmcau  24357  ulmdvlem1  24362  ulmdvlem3  24364  mtest  24366  mtestbdd  24367  pserval  24372  pserulm  24384  psercn  24388  pserdvlem2  24390  abelthlem3  24395  logtayl  24614  dvcxp1  24689  dvcncxp1  24692  logbmpt  24734  dmarea  24892  lgamgulmlem2  24964  lgamgulmlem5  24967  musum  25125  dchrptlem2  25198  dchrptlem3  25199  dchrpt  25200  lgsval  25234  lgsval4lem  25241  lgsneg  25254  lgsmod  25256  rpvmasum2  25409  padicfval  25513  ostth2  25534  ostth3  25535  ostth  25536  lmif  25885  islmib  25887  incistruhgr  26182  eucrct2eupth  27412  htthlem  28096  htth  28097  pjhfval  28577  hosmval  28916  hommval  28917  hodmval  28918  hfsmval  28919  hfmmval  28920  brafval  29124  kbfval  29133  psgnfzto1st  30174  mdetpmtr1  30208  ordtcnvNEW  30285  ordtrest2NEW  30288  xrhval  30381  indval  30394  esum2dlem  30473  ofceq  30478  itgeq12dv  30707  ballotlemfval  30870  vtsval  31034  ptpconn  31532  cvmliftlem15  31597  cvmlift2lem4  31605  cvmlift2  31615  snmlval  31630  snmlflim  31631  mrsubfval  31722  mrsubrn  31727  elmsubrn  31742  msubrn  31743  msubco  31745  faclim  31948  faclim2  31950  trpredeq1  32034  trpredeq2  32035  knoppcnlem1  32794  knoppcnlem6  32799  knoppcnlem7  32800  bj-evaleq  33329  csbrdgg  33486  curfv  33696  matunitlindflem2  33713  poimirlem5  33721  poimirlem6  33722  poimirlem7  33723  poimirlem8  33724  poimirlem10  33726  poimirlem11  33727  poimirlem12  33728  poimirlem15  33731  poimirlem16  33732  poimirlem17  33733  poimirlem18  33734  poimirlem19  33735  poimirlem20  33736  poimirlem21  33737  poimirlem22  33738  poimirlem27  33743  voliunnfl  33760  itg2addnclem  33767  itg2addnclem3  33769  itg2addnc  33770  itg2gt0cn  33771  iblabsnclem  33779  iblmulc2nc  33781  ftc1anclem2  33792  ftc1anclem6  33796  ftc1anclem8  33798  ftc1anc  33799  ftc2nc  33800  upixp  33830  rrncmslem  33936  ismrer1  33942  tendoplcbv  36550  tendopl  36551  tendoicbv  36568  tendoi  36569  dihfval  37006  lcfl7N  37276  lcfrlem8  37324  lcfrlem9  37325  lcf1o  37326  hvmapval  37535  hdmap1fval  37571  hdmapffval  37601  hdmapfval  37602  hgmapffval  37660  hgmapfval  37661  mzpclval  37784  mzpcl2  37789  mzpexpmpt  37804  mzpsubst  37807  mzpcompact2lem  37810  rmxfval  37964  rmyfval  37965  aomclem8  38126  hbtlem1  38188  hbtlem7  38190  itgpowd  38294  rfovfvd  38790  fsovrfovd  38797  fsovfvd  38798  fsovcnvlem  38801  dssmapfv2d  38806  dssmapnvod  38808  ntrneibex  38865  expgrowthi  39026  expgrowth  39028  binomcxplemdvsum  39048  addrval  39162  subrval  39163  mulvval  39164  fmulcl  40287  fmuldfeqlem1  40288  fprodcnlem  40305  fprodcn  40306  fnlimfv  40369  fnlimcnv  40373  fnlimfvre  40380  fnlimfvre2  40383  fnlimf  40384  fnlimabslt  40385  liminfval  40465  limsupresxr  40472  liminfresxr  40473  liminfvalxr  40489  fprodcncf  40588  dvnmptdivc  40627  dvnxpaek  40631  dvnmul  40632  dvmptfprod  40634  dvnprodlem1  40635  dvnprodlem2  40636  dvnprodlem3  40637  dvnprod  40638  stoweidlem2  40692  stoweidlem17  40707  stoweidlem19  40709  stoweidlem20  40710  stoweidlem43  40733  stoweidlem62  40752  stoweid  40753  dirkercncflem2  40794  fourierdlem112  40908  fourierdlem113  40909  etransclem1  40925  etransclem5  40929  etransclem17  40941  etransclem19  40943  etransclem22  40946  sge0val  41056  ovnlecvr  41248  ovncvrrp  41254  ovn0lem  41255  ovnsubaddlem1  41260  ovnsubadd  41262  hsphoif  41266  hsphoival  41269  hoidmv1lelem1  41281  hoidmv1lelem2  41282  hoidmv1lelem3  41283  hoidmv1le  41284  hoidmvlelem1  41285  hoidmvlelem2  41286  hoidmvlelem3  41287  hoidmvlelem4  41288  hoidmvlelem5  41289  hoidmvle  41290  ovnhoilem1  41291  ovnhoi  41293  hoidifhspval  41298  ovncvr2  41301  hoidifhspval2  41305  hspmbllem2  41317  hspmbllem3  41318  hspmbl  41319  ovnovollem1  41346  vonioolem2  41371  vonioo  41372  vonicclem2  41374  vonicc  41375  smflimlem4  41458  smflim  41461  smflim2  41488  smfsuplem2  41494  smfsup  41496  smfinf  41500  smflimsuplem2  41503  smflimsuplem5  41506  smflimsuplem7  41508  smflimsup  41510  c0rhm  42474  c0rnghm  42475  lincop  42759  aacllem  43112