Theorem mpteq2dv 4745

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

Syntax hints:   → wi 4   = wceq 1483   ∈ wcel 1990   ↦ cmpt 4729

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-ral 2917  df-opab 4713  df-mpt 4730

This theorem is referenced by:  ofeq  6899  mpt2curryvald  7396  rdgeq1  7507  rdgeq2  7508  omv  7592  oev  7594  oieq1  8417  oieq2  8418  cantnflem1  8586  wunex2  9560  wuncval2  9569  rpnnen1  11820  seqof2  12859  relexpsucnnr  13765  relexp1g  13766  limsupval  14205  sumeq2w  14422  sumeq2ii  14423  cbvsum  14425  summo  14448  fsum  14451  fsumrlim  14543  fsumo1  14544  prodeq2w  14642  prodmo  14666  fprod  14671  bpolylem  14779  rpnnen2lem1  14943  rpnnen2lem2  14944  1arithlem1  15627  vdwapval  15677  vdwlem6  15690  vdwlem8  15692  vdwlem9  15693  vdwlem10  15694  ramub1lem2  15731  ramcl  15733  sloteq  15862  prdsplusgval  16133  prdsmulrval  16135  prdsdsval  16138  prdsvscaval  16139  ismon  16393  fucco  16622  curf1  16865  curf2  16869  yonedalem4a  16915  grplactfval  17516  galactghm  17823  pmtrval  17871  sylow1  18018  sylow2b  18038  sylow3lem5  18046  sylow3  18048  iscyg  18281  gsumzaddlem  18321  gsumzmhm  18337  ablfac2  18488  gsumdixp  18609  fczpsrbag  19367  psrmulfval  19385  mvrval  19421  subrgmvr  19461  mplcoe1  19465  mplcoe3  19466  mplcoe5  19468  mplmon2  19493  subrgascl  19498  evlslem2  19512  evlslem3  19514  evlslem1  19515  mpfrcl  19518  evlsval  19519  evlsvar  19523  mpfind  19536  coe1fval  19575  pf1ind  19719  evl1gsumadd  19722  zncyg  19897  phllmhm  19977  isphld  19999  frlmgsum  20111  frlmipval  20118  frlmphl  20120  uvcval  20124  mamuval  20192  mamufv  20193  matgsum  20243  madetsumid  20267  mat1dimmul  20282  mvmulval  20349  mvmulfv  20350  mavmulfv  20352  1mavmul  20354  marepvval0  20372  mulmarep1gsum1  20379  mdetleib  20393  mdetleib2  20394  mdetfval1  20396  mdetleib1  20397  mdet0pr  20398  m1detdiag  20403  mdetralt  20414  mdetunilem9  20426  m2detleib  20437  smadiadetlem3  20474  mat2pmatmul  20536  decpmatmul  20577  decpmatmulsumfsupp  20578  pmatcollpw1  20581  monmatcollpw  20584  pmatcollpw3lem  20588  pmatcollpw3fi1lem2  20592  pm2mpval  20600  pm2mpfval  20601  mply1topmatval  20609  mp2pm2mplem1  20611  mp2pm2mplem3  20613  ptbasfi  21384  ptcnplem  21424  ptrescn  21442  cnmpt2k  21491  xkohmeo  21618  fmval  21747  fmf  21749  ptcmpg  21861  tmdmulg  21896  prdstmdd  21927  tsmspropd  21935  prdsxmslem2  22334  metdsval  22650  fsumcn  22673  expcn  22675  lebnumlem3  22762  pcoval  22811  pi1xfrcnv  22857  rrxds  23181  rrxmval  23188  itg11  23458  mbfi1fseqlem2  23483  mbfi1fseqlem6  23487  mbfi1fseq  23488  mbfi1flimlem  23489  mbfmullem  23492  itg2const  23507  itg2mulc  23514  itg2monolem1  23517  itg2i1fseqle  23521  itg2i1fseq  23522  itg2addlem  23525  itg2cnlem1  23528  itg2cn  23530  isibl  23532  isibl2  23533  iblitg  23535  itgz  23547  itgvallem  23551  itgvallem3  23552  iblcnlem1  23554  itgcnlem  23556  iblrelem  23557  iblposlem  23558  iblpos  23559  itgrevallem1  23561  itgposval  23562  iblss2  23572  itgss  23578  itgfsum  23593  iblabslem  23594  iblmulc2  23597  bddmulibl  23605  itgcn  23609  ellimc  23637  dvnfval  23685  cpnfval  23695  dvexp  23716  dvexp2  23717  dvmptfsum  23738  dvlipcn  23757  dvivthlem1  23771  dvfsumle  23784  dvfsumabs  23786  dvfsumlem2  23790  elply2  23952  elplyr  23957  elplyd  23958  coeeu  23981  coelem  23982  coeeq  23983  plyco  23997  coe11  24009  coe1termlem  24014  dgrcolem1  24029  dvply2g  24040  elqaalem3  24076  eltayl  24114  tayl0  24116  taylthlem1  24127  taylthlem2  24128  ulmcau  24149  ulmdvlem1  24154  ulmdvlem3  24156  mtest  24158  mtestbdd  24159  pserval  24164  pserulm  24176  psercn  24180  pserdvlem2  24182  abelthlem3  24187  logtayl  24406  dvcxp1  24481  dvcncxp1  24484  logbmpt  24526  dmarea  24684  lgamgulmlem2  24756  lgamgulmlem5  24759  musum  24917  dchrptlem2  24990  dchrptlem3  24991  dchrpt  24992  lgsval  25026  lgsval4lem  25033  lgsneg  25046  lgsmod  25048  rpvmasum2  25201  padicfval  25305  ostth2  25326  ostth3  25327  ostth  25328  lmif  25677  islmib  25679  incistruhgr  25974  eucrct2eupth  27105  htthlem  27774  htth  27775  pjhfval  28255  hosmval  28594  hommval  28595  hodmval  28596  hfsmval  28597  hfmmval  28598  brafval  28802  kbfval  28811  psgnfzto1st  29855  mdetpmtr1  29889  ordtcnvNEW  29966  ordtrest2NEW  29969  xrhval  30062  indval  30075  esum2dlem  30154  ofceq  30159  itgeq12dv  30388  ballotlemfval  30551  vtsval  30715  ptpconn  31215  cvmliftlem15  31280  cvmlift2lem4  31288  cvmlift2  31298  snmlval  31313  snmlflim  31314  mrsubfval  31405  mrsubrn  31410  elmsubrn  31425  msubrn  31426  msubco  31428  faclim  31632  faclim2  31634  trpredeq1  31720  trpredeq2  31721  knoppcnlem1  32483  knoppcnlem6  32488  knoppcnlem7  32489  bj-evaleq  33024  csbrdgg  33175  curfv  33389  matunitlindflem2  33406  poimirlem5  33414  poimirlem6  33415  poimirlem7  33416  poimirlem8  33417  poimirlem10  33419  poimirlem11  33420  poimirlem12  33421  poimirlem15  33424  poimirlem16  33425  poimirlem17  33426  poimirlem18  33427  poimirlem19  33428  poimirlem20  33429  poimirlem21  33430  poimirlem22  33431  poimirlem27  33436  voliunnfl  33453  itg2addnclem  33461  itg2addnclem3  33463  itg2addnc  33464  itg2gt0cn  33465  iblabsnclem  33473  iblmulc2nc  33475  ftc1anclem2  33486  ftc1anclem6  33490  ftc1anclem8  33492  ftc1anc  33493  ftc2nc  33494  upixp  33524  rrncmslem  33631  ismrer1  33637  tendoplcbv  36063  tendopl  36064  tendoicbv  36081  tendoi  36082  dihfval  36520  lcfl7N  36790  lcfrlem8  36838  lcfrlem9  36839  lcf1o  36840  hvmapval  37049  hdmap1fval  37086  hdmapffval  37118  hdmapfval  37119  hgmapffval  37177  hgmapfval  37178  mzpclval  37288  mzpcl2  37293  mzpexpmpt  37308  mzpsubst  37311  mzpcompact2lem  37314  rmxfval  37468  rmyfval  37469  aomclem8  37631  hbtlem1  37693  hbtlem7  37695  itgpowd  37800  rfovfvd  38296  fsovrfovd  38303  fsovfvd  38304  fsovcnvlem  38307  dssmapfv2d  38312  dssmapnvod  38314  ntrneibex  38371  expgrowthi  38532  expgrowth  38534  binomcxplemdvsum  38554  addrval  38670  subrval  38671  mulvval  38672  fmulcl  39813  fmuldfeqlem1  39814  fprodcnlem  39831  fprodcn  39832  fnlimfv  39895  fnlimcnv  39899  fnlimfvre  39906  fnlimfvre2  39909  fnlimf  39910  fnlimabslt  39911  liminfval  39991  limsupresxr  39998  liminfresxr  39999  liminfvalxr  40015  fprodcncf  40114  dvnmptdivc  40153  dvnxpaek  40157  dvnmul  40158  dvmptfprod  40160  dvnprodlem1  40161  dvnprodlem2  40162  dvnprodlem3  40163  dvnprod  40164  stoweidlem2  40219  stoweidlem17  40234  stoweidlem19  40236  stoweidlem20  40237  stoweidlem43  40260  stoweidlem62  40279  stoweid  40280  dirkercncflem2  40321  fourierdlem112  40435  fourierdlem113  40436  etransclem1  40452  etransclem5  40456  etransclem17  40468  etransclem19  40470  etransclem22  40473  sge0val  40583  ovnlecvr  40772  ovncvrrp  40778  ovn0lem  40779  ovnsubaddlem1  40784  ovnsubadd  40786  hsphoif  40790  hsphoival  40793  hoidmv1lelem1  40805  hoidmv1lelem2  40806  hoidmv1lelem3  40807  hoidmv1le  40808  hoidmvlelem1  40809  hoidmvlelem2  40810  hoidmvlelem3  40811  hoidmvlelem4  40812  hoidmvlelem5  40813  hoidmvle  40814  ovnhoilem1  40815  ovnhoi  40817  hoidifhspval  40822  ovncvr2  40825  hoidifhspval2  40829  hspmbllem2  40841  hspmbllem3  40842  hspmbl  40843  ovnovollem1  40870  vonioolem2  40895  vonioo  40896  vonicclem2  40898  vonicc  40899  smflimlem4  40982  smflim  40985  smflim2  41012  smfsuplem2  41018  smfsup  41020  smfinf  41024  smflimsuplem2  41027  smflimsuplem5  41030  smflimsuplem7  41032  smflimsup  41034  c0rhm  41912  c0rnghm  41913  lincop  42197  aacllem  42547