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

Syntax hints:   → wi 4   = wceq 1536   ∈ wcel 2105   ↦ cmpt 5230

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-opab 5210  df-mpt 5231

This theorem is referenced by:  ofeqd  7698  mpocurryvald  8293  rdgeq1  8449  rdgeq2  8450  omv  8548  oev  8550  oieq1  9549  oieq2  9550  cantnflem1  9726  wunex2  10775  wuncval2  10784  rpnnen1  13022  seqof2  14097  relexpsucnnr  15060  relexp1g  15061  limsupval  15506  sumeq2w  15724  sumeq2ii  15725  cbvsum  15727  cbvsumv  15728  sumeq2sdv  15735  summo  15749  fsum  15752  fsumrlim  15843  fsumo1  15844  prodeq1  15939  prodeq2w  15942  prodeq2sdv  15955  prodmo  15968  fprod  15973  bpolylem  16080  rpnnen2lem1  16246  rpnnen2lem2  16247  1arithlem1  16956  vdwapval  17006  vdwlem6  17019  vdwlem8  17021  vdwlem9  17022  vdwlem10  17023  ramub1lem2  17060  ramcl  17062  sloteq  17216  prdsplusgval  17519  prdsmulrval  17521  prdsdsval  17524  prdsvscaval  17525  ismon  17780  fucco  18018  curf1  18281  curf2  18285  yonedalem4a  18331  smndex1gbas  18927  smndex1gid  18928  grplactfval  19071  galactghm  19436  pmtrval  19483  sylow1  19635  sylow2b  19655  sylow3lem5  19663  sylow3  19665  iscyg  19911  gsumzaddlem  19953  gsumzmhm  19969  ablfac2  20123  gsumdixp  20332  c0rhm  20550  c0rnghm  20551  zncyg  21584  phllmhm  21667  isphld  21689  frlmgsum  21809  frlmipval  21816  frlmphl  21818  uvcval  21822  fczpsrbag  21958  psrmulfval  21980  psrascl  22016  mvrval  22019  subrgmvr  22068  mplcoe1  22072  mplcoe3  22073  mplcoe5  22075  mplmon2  22102  subrgascl  22107  evlslem2  22120  evlslem3  22121  evlslem1  22123  mpfrcl  22126  evlsval  22127  evlsvar  22131  mpfind  22148  selvfval  22155  selvval  22156  mhpfval  22159  psdfval  22179  psdval  22180  coe1fval  22222  pf1ind  22374  evl1gsumadd  22377  rhmmpl  22402  rhmply1vr1  22406  mamuval  22412  mamufv  22413  matgsum  22458  madetsumid  22482  mat1dimmul  22497  mvmulval  22564  mvmulfv  22565  mavmulfv  22567  1mavmul  22569  marepvval0  22587  mulmarep1gsum1  22594  mdetleib  22608  mdetleib2  22609  mdetfval1  22611  mdetleib1  22612  mdet0pr  22613  m1detdiag  22618  mdetralt  22629  mdetunilem9  22641  m2detleib  22652  smadiadetlem3  22689  mat2pmatmul  22752  decpmatmul  22793  decpmatmulsumfsupp  22794  pmatcollpw1  22797  monmatcollpw  22800  pmatcollpw3lem  22804  pmatcollpw3fi1lem2  22808  pm2mpval  22816  pm2mpfval  22817  mply1topmatval  22825  mp2pm2mplem1  22827  mp2pm2mplem3  22829  ptbasfi  23604  ptcnplem  23644  ptrescn  23662  cnmpt2k  23711  xkohmeo  23838  fmval  23966  fmf  23968  ptcmpg  24080  tmdmulg  24115  prdstmdd  24147  tsmspropd  24155  prdsxmslem2  24557  metdsval  24882  fsumcn  24907  expcn  24909  expcnOLD  24911  lebnumlem3  25008  pcoval  25057  pi1xfrcnv  25103  cphsscph  25298  rrxds  25440  rrxmval  25452  itg11  25739  mbfi1fseqlem2  25765  mbfi1fseqlem6  25769  mbfi1fseq  25770  mbfi1flimlem  25771  mbfmullem  25774  itg2const  25789  itg2mulc  25796  itg2monolem1  25799  itg2i1fseqle  25803  itg2i1fseq  25804  itg2addlem  25807  itg2cnlem1  25810  itg2cn  25812  isibl  25814  isibl2  25815  iblitg  25817  itgeq1  25822  itgz  25830  itgvallem  25834  itgvallem3  25835  iblcnlem1  25837  itgcnlem  25839  iblrelem  25840  iblposlem  25841  iblpos  25842  itgrevallem1  25844  itgposval  25845  iblss2  25855  itgss  25861  itgfsum  25876  iblabslem  25877  iblmulc2  25880  bddmulibl  25888  itgcn  25894  ellimc  25922  dvnfval  25972  cpnfval  25982  dvexp  26005  dvexp2  26006  dvmptfsum  26027  dvlipcn  26047  dvivthlem1  26061  dvfsumle  26074  dvfsumleOLD  26075  dvfsumabs  26077  dvfsumlem2  26081  dvfsumlem2OLD  26082  itgpowd  26105  elply2  26249  elplyr  26254  elplyd  26255  coeeu  26278  coelem  26279  coeeq  26280  plyco  26294  coe11  26306  coe1termlem  26311  dgrcolem1  26327  dvply2g  26340  dvply2gOLD  26341  elqaalem3  26377  eltayl  26415  tayl0  26417  taylthlem1  26429  taylthlem2  26430  taylthlem2OLD  26431  ulmcau  26452  ulmdvlem1  26457  ulmdvlem3  26459  mtest  26461  mtestbdd  26462  pserval  26467  pserulm  26479  psercn  26484  pserdvlem2  26486  abelthlem3  26491  logtayl  26716  dvcxp1  26796  dvcncxp1  26799  logbmpt  26845  dmarea  27014  lgamgulmlem2  27087  lgamgulmlem5  27090  musum  27248  dchrptlem2  27323  dchrptlem3  27324  dchrpt  27325  lgsval  27359  lgsval4lem  27366  lgsneg  27379  lgsmod  27381  rpvmasum2  27570  padicfval  27674  ostth2  27695  ostth3  27696  ostth  27697  lmif  28807  islmib  28809  incistruhgr  29110  eucrct2eupth  30273  htthlem  30945  htth  30946  pjhfval  31424  hosmval  31763  hommval  31764  hodmval  31765  hfsmval  31766  hfmmval  31767  brafval  31971  kbfval  31980  mptprop  32712  psgnfzto1st  33107  elrgspnlem1  33231  elrgspnlem2  33232  elrgspnlem3  33233  elrgspnlem4  33234  elrgspn  33235  linds2eq  33388  elrspunidl  33435  elrspunsn  33436  evl1deg1  33580  evl1deg2  33581  evl1deg3  33582  lbsdiflsp0  33653  fedgmullem1  33656  fedgmullem2  33657  fedgmul  33658  evls1fldgencl  33694  mdetpmtr1  33783  zar0ring  33838  ordtcnvNEW  33880  ordtrest2NEW  33883  xrhval  33980  indval  33993  esum2dlem  34072  ofceq  34077  itgeq12dv  34307  ballotlemfval  34470  vtsval  34630  lpadval  34669  ptpconn  35217  cvmliftlem15  35282  cvmlift2lem4  35290  cvmlift2  35300  snmlval  35315  snmlflim  35316  satf  35337  mrsubfval  35492  mrsubrn  35497  elmsubrn  35512  msubrn  35513  msubco  35515  faclim  35725  faclim2  35727  prodeq12sdv  36200  itgeq12sdv  36201  cbvsumdavw  36261  cbvproddavw  36262  cbvsumdavw2  36277  cbvproddavw2  36278  knoppcnlem1  36475  knoppcnlem6  36480  knoppcnlem7  36481  bj-evaleq  37054  csbrdgg  37311  curfv  37586  matunitlindflem2  37603  poimirlem5  37611  poimirlem6  37612  poimirlem7  37613  poimirlem8  37614  poimirlem10  37616  poimirlem11  37617  poimirlem12  37618  poimirlem15  37621  poimirlem16  37622  poimirlem17  37623  poimirlem18  37624  poimirlem19  37625  poimirlem20  37626  poimirlem21  37627  poimirlem22  37628  poimirlem27  37633  voliunnfl  37650  itg2addnclem  37657  itg2addnclem3  37659  itg2addnc  37660  itg2gt0cn  37661  iblabsnclem  37669  iblmulc2nc  37671  ftc1anclem2  37680  ftc1anclem6  37684  ftc1anclem8  37686  ftc1anc  37687  ftc2nc  37688  upixp  37715  rrncmslem  37818  ismrer1  37824  tendoplcbv  40757  tendopl  40758  tendoicbv  40775  tendoi  40776  dihfval  41213  lcfl7N  41483  lcfrlem8  41531  lcfrlem9  41532  lcf1o  41533  hvmapval  41742  hdmap1fval  41778  hdmapffval  41808  hdmapfval  41809  hgmapffval  41867  hgmapfval  41868  lcmineqlem7  42016  lcmineqlem12  42021  aks6d1c6lem5  42158  rhmpsr  42538  evlsvval  42546  evlsvvval  42549  evlsbagval  42552  selvvvval  42571  evlselv  42573  fsuppind  42576  fsuppssindlem2  42578  fsuppssind  42579  mzpclval  42712  mzpcl2  42717  mzpexpmpt  42732  mzpsubst  42735  mzpcompact2lem  42738  rmxfval  42891  rmyfval  42892  aomclem8  43049  hbtlem1  43111  hbtlem7  43113  rfovfvd  43991  fsovrfovd  43998  fsovfvd  43999  fsovcnvlem  44002  dssmapfv2d  44007  dssmapnvod  44009  ntrneibex  44062  mnringmulrvald  44222  mnringmulrcld  44223  expgrowthi  44328  expgrowth  44330  binomcxplemdvsum  44350  addrval  44461  subrval  44462  mulvval  44463  fmulcl  45536  fmuldfeqlem1  45537  fprodcnlem  45554  fprodcn  45555  fnlimfv  45618  fnlimcnv  45622  fnlimfvre  45629  fnlimfvre2  45632  fnlimf  45633  fnlimabslt  45634  liminfval  45714  limsupresxr  45721  liminfresxr  45722  liminfvalxr  45738  fprodcncf  45855  dvnmptdivc  45893  dvnxpaek  45897  dvnmul  45898  dvmptfprod  45900  dvnprodlem1  45901  dvnprodlem2  45902  dvnprodlem3  45903  dvnprod  45904  stoweidlem2  45957  stoweidlem17  45972  stoweidlem19  45974  stoweidlem20  45975  stoweidlem43  45998  stoweidlem62  46017  stoweid  46018  dirkercncflem2  46059  fourierdlem112  46173  fourierdlem113  46174  etransclem1  46190  etransclem5  46194  etransclem17  46206  etransclem19  46208  etransclem22  46211  sge0val  46321  ovnlecvr  46513  ovncvrrp  46519  ovn0lem  46520  ovnsubaddlem1  46525  ovnsubadd  46527  hsphoif  46531  hsphoival  46534  hoidmv1lelem1  46546  hoidmv1lelem2  46547  hoidmv1lelem3  46548  hoidmv1le  46549  hoidmvlelem1  46550  hoidmvlelem2  46551  hoidmvlelem3  46552  hoidmvlelem4  46553  hoidmvlelem5  46554  hoidmvle  46555  ovnhoilem1  46556  ovnhoi  46558  hoidifhspval  46563  ovncvr2  46566  hoidifhspval2  46570  hspmbllem2  46582  hspmbllem3  46583  hspmbl  46584  ovnovollem1  46611  vonioolem2  46636  vonioo  46637  vonicclem2  46639  vonicc  46640  smflimlem4  46729  smflim  46732  smflim2  46761  smfsuplem2  46767  smfsup  46769  smfinf  46773  smflimsuplem2  46776  smflimsuplem5  46779  smflimsuplem7  46781  smflimsup  46783  cfsetsnfsetfo  47009  lincop  48253  1arymaptfv  48489  itcoval  48510  itcovalpc  48521  itcovalt2  48526  ackvalsuc1mpt  48527  ackval1  48530  aacllem  49031