Theorem mpteq2dv 5249

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2104   ↦ cmpt 5230

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-opab 5210  df-mpt 5231

This theorem is referenced by:  ofeqd  7674  mpocurryvald  8257  rdgeq1  8413  rdgeq2  8414  omv  8514  oev  8516  oieq1  9509  oieq2  9510  cantnflem1  9686  wunex2  10735  wuncval2  10744  rpnnen1  12971  seqof2  14030  relexpsucnnr  14976  relexp1g  14977  limsupval  15422  sumeq2w  15642  sumeq2ii  15643  cbvsum  15645  summo  15667  fsum  15670  fsumrlim  15761  fsumo1  15762  prodeq2w  15860  prodmo  15884  fprod  15889  bpolylem  15996  rpnnen2lem1  16161  rpnnen2lem2  16162  1arithlem1  16860  vdwapval  16910  vdwlem6  16923  vdwlem8  16925  vdwlem9  16926  vdwlem10  16927  ramub1lem2  16964  ramcl  16966  sloteq  17120  prdsplusgval  17423  prdsmulrval  17425  prdsdsval  17428  prdsvscaval  17429  ismon  17684  fucco  17919  curf1  18182  curf2  18186  yonedalem4a  18232  smndex1gbas  18819  smndex1gid  18820  grplactfval  18960  galactghm  19313  pmtrval  19360  sylow1  19512  sylow2b  19532  sylow3lem5  19540  sylow3  19542  iscyg  19788  gsumzaddlem  19830  gsumzmhm  19846  ablfac2  20000  gsumdixp  20207  c0rhm  20423  c0rnghm  20424  zncyg  21323  phllmhm  21404  isphld  21426  frlmgsum  21546  frlmipval  21553  frlmphl  21555  uvcval  21559  fczpsrbag  21695  psrmulfval  21723  mvrval  21760  subrgmvr  21807  mplcoe1  21811  mplcoe3  21812  mplcoe5  21814  mplmon2  21841  subrgascl  21846  evlslem2  21861  evlslem3  21862  evlslem1  21864  mpfrcl  21867  evlsval  21868  evlsvar  21872  mpfind  21889  selvfval  21899  selvval  21900  mhpfval  21901  coe1fval  21948  pf1ind  22094  evl1gsumadd  22097  mamuval  22108  mamufv  22109  matgsum  22159  madetsumid  22183  mat1dimmul  22198  mvmulval  22265  mvmulfv  22266  mavmulfv  22268  1mavmul  22270  marepvval0  22288  mulmarep1gsum1  22295  mdetleib  22309  mdetleib2  22310  mdetfval1  22312  mdetleib1  22313  mdet0pr  22314  m1detdiag  22319  mdetralt  22330  mdetunilem9  22342  m2detleib  22353  smadiadetlem3  22390  mat2pmatmul  22453  decpmatmul  22494  decpmatmulsumfsupp  22495  pmatcollpw1  22498  monmatcollpw  22501  pmatcollpw3lem  22505  pmatcollpw3fi1lem2  22509  pm2mpval  22517  pm2mpfval  22518  mply1topmatval  22526  mp2pm2mplem1  22528  mp2pm2mplem3  22530  ptbasfi  23305  ptcnplem  23345  ptrescn  23363  cnmpt2k  23412  xkohmeo  23539  fmval  23667  fmf  23669  ptcmpg  23781  tmdmulg  23816  prdstmdd  23848  tsmspropd  23856  prdsxmslem2  24258  metdsval  24583  fsumcn  24608  expcn  24610  expcnOLD  24612  lebnumlem3  24709  pcoval  24758  pi1xfrcnv  24804  cphsscph  24999  rrxds  25141  rrxmval  25153  itg11  25440  mbfi1fseqlem2  25466  mbfi1fseqlem6  25470  mbfi1fseq  25471  mbfi1flimlem  25472  mbfmullem  25475  itg2const  25490  itg2mulc  25497  itg2monolem1  25500  itg2i1fseqle  25504  itg2i1fseq  25505  itg2addlem  25508  itg2cnlem1  25511  itg2cn  25513  isibl  25515  isibl2  25516  iblitg  25518  itgz  25530  itgvallem  25534  itgvallem3  25535  iblcnlem1  25537  itgcnlem  25539  iblrelem  25540  iblposlem  25541  iblpos  25542  itgrevallem1  25544  itgposval  25545  iblss2  25555  itgss  25561  itgfsum  25576  iblabslem  25577  iblmulc2  25580  bddmulibl  25588  itgcn  25594  ellimc  25622  dvnfval  25672  cpnfval  25682  dvexp  25705  dvexp2  25706  dvmptfsum  25727  dvlipcn  25746  dvivthlem1  25760  dvfsumle  25773  dvfsumabs  25775  dvfsumlem2  25779  itgpowd  25802  elply2  25945  elplyr  25950  elplyd  25951  coeeu  25974  coelem  25975  coeeq  25976  plyco  25990  coe11  26002  coe1termlem  26007  dgrcolem1  26023  dvply2g  26034  elqaalem3  26070  eltayl  26108  tayl0  26110  taylthlem1  26121  taylthlem2  26122  ulmcau  26143  ulmdvlem1  26148  ulmdvlem3  26150  mtest  26152  mtestbdd  26153  pserval  26158  pserulm  26170  psercn  26174  pserdvlem2  26176  abelthlem3  26181  logtayl  26404  dvcxp1  26484  dvcncxp1  26487  logbmpt  26529  dmarea  26698  lgamgulmlem2  26770  lgamgulmlem5  26773  musum  26931  dchrptlem2  27004  dchrptlem3  27005  dchrpt  27006  lgsval  27040  lgsval4lem  27047  lgsneg  27060  lgsmod  27062  rpvmasum2  27251  padicfval  27355  ostth2  27376  ostth3  27377  ostth  27378  lmif  28303  islmib  28305  incistruhgr  28606  eucrct2eupth  29765  htthlem  30437  htth  30438  pjhfval  30916  hosmval  31255  hommval  31256  hodmval  31257  hfsmval  31258  hfmmval  31259  brafval  31463  kbfval  31472  mptprop  32187  psgnfzto1st  32534  linds2eq  32771  elrspunidl  32820  elrspunsn  32821  lbsdiflsp0  32999  fedgmullem1  33002  fedgmullem2  33003  fedgmul  33004  evls1fldgencl  33033  mdetpmtr1  33101  zar0ring  33156  ordtcnvNEW  33198  ordtrest2NEW  33201  xrhval  33296  indval  33309  esum2dlem  33388  ofceq  33393  itgeq12dv  33623  ballotlemfval  33786  vtsval  33947  lpadval  33986  ptpconn  34522  cvmliftlem15  34587  cvmlift2lem4  34595  cvmlift2  34605  snmlval  34620  snmlflim  34621  satf  34642  mrsubfval  34797  mrsubrn  34802  elmsubrn  34817  msubrn  34818  msubco  34820  faclim  35020  faclim2  35022  gg-dvfsumle  35468  gg-dvfsumlem2  35469  knoppcnlem1  35672  knoppcnlem6  35677  knoppcnlem7  35678  bj-evaleq  36256  csbrdgg  36513  curfv  36771  matunitlindflem2  36788  poimirlem5  36796  poimirlem6  36797  poimirlem7  36798  poimirlem8  36799  poimirlem10  36801  poimirlem11  36802  poimirlem12  36803  poimirlem15  36806  poimirlem16  36807  poimirlem17  36808  poimirlem18  36809  poimirlem19  36810  poimirlem20  36811  poimirlem21  36812  poimirlem22  36813  poimirlem27  36818  voliunnfl  36835  itg2addnclem  36842  itg2addnclem3  36844  itg2addnc  36845  itg2gt0cn  36846  iblabsnclem  36854  iblmulc2nc  36856  ftc1anclem2  36865  ftc1anclem6  36869  ftc1anclem8  36871  ftc1anc  36872  ftc2nc  36873  upixp  36900  rrncmslem  37003  ismrer1  37009  tendoplcbv  39949  tendopl  39950  tendoicbv  39967  tendoi  39968  dihfval  40405  lcfl7N  40675  lcfrlem8  40723  lcfrlem9  40724  lcf1o  40725  hvmapval  40934  hdmap1fval  40970  hdmapffval  41000  hdmapfval  41001  hgmapffval  41059  hgmapfval  41060  lcmineqlem7  41206  lcmineqlem12  41211  rhmmpl  41427  evlsvval  41434  evlsvvval  41437  evlsbagval  41440  selvvvval  41459  evlselv  41461  fsuppind  41464  fsuppssindlem2  41466  fsuppssind  41467  mzpclval  41765  mzpcl2  41770  mzpexpmpt  41785  mzpsubst  41788  mzpcompact2lem  41791  rmxfval  41944  rmyfval  41945  aomclem8  42105  hbtlem1  42167  hbtlem7  42169  rfovfvd  43055  fsovrfovd  43062  fsovfvd  43063  fsovcnvlem  43066  dssmapfv2d  43071  dssmapnvod  43073  ntrneibex  43126  mnringmulrvald  43288  mnringmulrcld  43289  expgrowthi  43394  expgrowth  43396  binomcxplemdvsum  43416  addrval  43527  subrval  43528  mulvval  43529  fmulcl  44595  fmuldfeqlem1  44596  fprodcnlem  44613  fprodcn  44614  fnlimfv  44677  fnlimcnv  44681  fnlimfvre  44688  fnlimfvre2  44691  fnlimf  44692  fnlimabslt  44693  liminfval  44773  limsupresxr  44780  liminfresxr  44781  liminfvalxr  44797  fprodcncf  44914  dvnmptdivc  44952  dvnxpaek  44956  dvnmul  44957  dvmptfprod  44959  dvnprodlem1  44960  dvnprodlem2  44961  dvnprodlem3  44962  dvnprod  44963  stoweidlem2  45016  stoweidlem17  45031  stoweidlem19  45033  stoweidlem20  45034  stoweidlem43  45057  stoweidlem62  45076  stoweid  45077  dirkercncflem2  45118  fourierdlem112  45232  fourierdlem113  45233  etransclem1  45249  etransclem5  45253  etransclem17  45265  etransclem19  45267  etransclem22  45270  sge0val  45380  ovnlecvr  45572  ovncvrrp  45578  ovn0lem  45579  ovnsubaddlem1  45584  ovnsubadd  45586  hsphoif  45590  hsphoival  45593  hoidmv1lelem1  45605  hoidmv1lelem2  45606  hoidmv1lelem3  45607  hoidmv1le  45608  hoidmvlelem1  45609  hoidmvlelem2  45610  hoidmvlelem3  45611  hoidmvlelem4  45612  hoidmvlelem5  45613  hoidmvle  45614  ovnhoilem1  45615  ovnhoi  45617  hoidifhspval  45622  ovncvr2  45625  hoidifhspval2  45629  hspmbllem2  45641  hspmbllem3  45642  hspmbl  45643  ovnovollem1  45670  vonioolem2  45695  vonioo  45696  vonicclem2  45698  vonicc  45699  smflimlem4  45788  smflim  45791  smflim2  45820  smfsuplem2  45826  smfsup  45828  smfinf  45832  smflimsuplem2  45835  smflimsuplem5  45838  smflimsuplem7  45840  smflimsup  45842  cfsetsnfsetfo  46068  lincop  47176  1arymaptfv  47413  itcoval  47434  itcovalpc  47445  itcovalt2  47450  ackvalsuc1mpt  47451  ackval1  47454  aacllem  47935