Theorem mpteq2dv 5166

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

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119   ↦ cmpt 5153

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-opab 5135  df-mpt 5154

This theorem is referenced by:  ifmpt2v  7458  ofeqd  7622  mpocurryvald  8210  rdgeq1  8340  rdgeq2  8341  omv  8437  oev  8439  oieq1  9417  oieq2  9418  cantnflem1  9601  wunex2  10652  wuncval2  10661  indval  12153  rpnnen1  12924  seqof2  14013  relexpsucnnr  14978  relexp1g  14979  limsupval  15427  sumeq2w  15645  sumeq2ii  15646  cbvsum  15648  cbvsumv  15649  sumeq2sdv  15656  summo  15670  fsum  15673  fsumrlim  15765  fsumo1  15766  prodeq1  15863  prodeq2w  15866  prodeq2sdv  15879  prodmo  15892  fprod  15897  bpolylem  16004  rpnnen2lem1  16172  rpnnen2lem2  16173  1arithlem1  16885  vdwapval  16935  vdwlem6  16948  vdwlem8  16950  vdwlem9  16951  vdwlem10  16952  ramub1lem2  16989  ramcl  16991  sloteq  17144  prdsplusgval  17427  prdsmulrval  17429  prdsdsval  17432  prdsvscaval  17433  ismon  17691  fucco  17923  curf1  18182  curf2  18186  yonedalem4a  18232  smndex1gbas  18861  smndex1gbasOLD  18862  smndex1gid  18863  smndex1gidOLD  18864  smndex1igid  18865  grplactfval  19008  galactghm  19370  pmtrval  19417  sylow1  19569  sylow2b  19589  sylow3lem5  19597  sylow3  19599  iscyg  19845  gsumzaddlem  19887  gsumzmhm  19903  ablfac2  20057  gsumdixp  20289  c0rhm  20506  c0rnghm  20507  zncyg  21523  phllmhm  21607  isphld  21629  frlmgsum  21747  frlmipval  21754  frlmphl  21756  uvcval  21760  fczpsrbag  21896  psrmulfval  21918  psrascl  21953  mvrval  21956  subrgmvr  22009  mplcoe1  22013  mplcoe3  22014  mplcoe5  22016  mplmon2  22037  subrgascl  22042  evlslem2  22055  evlslem3  22056  evlslem1  22058  mpfrcl  22061  evlsval  22062  evlsvval  22066  evlsvvval  22069  evlsvar  22071  mpfind  22091  selvfval  22095  selvval  22096  selvvvval  22118  mhpfval  22126  psdfval  22146  psdval  22147  psdmvr  22157  coe1fval  22190  pf1ind  22341  evl1gsumadd  22344  rhmmpl  22366  rhmply1vr1  22370  mamuval  22376  mamufv  22377  matgsum  22420  madetsumid  22444  mat1dimmul  22459  mvmulval  22526  mvmulfv  22527  mavmulfv  22529  1mavmul  22531  marepvval0  22549  mulmarep1gsum1  22556  mdetleib  22570  mdetleib2  22571  mdetfval1  22573  mdetleib1  22574  mdet0pr  22575  m1detdiag  22580  mdetralt  22591  mdetunilem9  22603  m2detleib  22614  smadiadetlem3  22651  mat2pmatmul  22714  decpmatmul  22755  decpmatmulsumfsupp  22756  pmatcollpw1  22759  monmatcollpw  22762  pmatcollpw3lem  22766  pmatcollpw3fi1lem2  22770  pm2mpval  22778  pm2mpfval  22779  mply1topmatval  22787  mp2pm2mplem1  22789  mp2pm2mplem3  22791  ptbasfi  23564  ptcnplem  23604  ptrescn  23622  cnmpt2k  23671  xkohmeo  23798  fmval  23926  fmf  23928  ptcmpg  24040  tmdmulg  24075  prdstmdd  24107  tsmspropd  24115  prdsxmslem2  24512  metdsval  24831  fsumcn  24855  expcn  24857  lebnumlem3  24948  pcoval  24996  pi1xfrcnv  25042  cphsscph  25236  rrxds  25378  rrxmval  25390  itg11  25676  mbfi1fseqlem2  25701  mbfi1fseqlem6  25705  mbfi1fseq  25706  mbfi1flimlem  25707  mbfmullem  25710  itg2const  25725  itg2mulc  25732  itg2monolem1  25735  itg2i1fseqle  25739  itg2i1fseq  25740  itg2addlem  25743  itg2cnlem1  25746  itg2cn  25748  isibl  25750  isibl2  25751  iblitg  25753  itgeq1  25758  itgz  25766  itgvallem  25770  itgvallem3  25771  iblcnlem1  25773  itgcnlem  25775  iblrelem  25776  iblposlem  25777  iblpos  25778  itgrevallem1  25780  itgposval  25781  iblss2  25791  itgss  25797  itgfsum  25812  iblabslem  25813  iblmulc2  25816  bddmulibl  25824  itgcn  25830  ellimc  25858  dvnfval  25907  cpnfval  25917  dvexp  25938  dvexp2  25939  dvmptfsum  25960  dvlipcn  25979  dvivthlem1  25993  dvfsumle  26006  dvfsumabs  26008  dvfsumlem2  26012  itgpowd  26035  elply2  26179  elplyr  26184  elplyd  26185  coeeu  26208  coelem  26209  coeeq  26210  plyco  26224  coe11  26236  coe1termlem  26241  dgrcolem1  26256  dvply2g  26269  elqaalem3  26305  eltayl  26343  tayl0  26345  taylthlem1  26356  taylthlem2  26357  ulmcau  26378  ulmdvlem1  26383  ulmdvlem3  26385  mtest  26387  mtestbdd  26388  pserval  26393  pserulm  26405  psercn  26409  pserdvlem2  26411  abelthlem3  26416  logtayl  26642  dvcxp1  26722  dvcncxp1  26725  logbmpt  26770  dmarea  26939  lgamgulmlem2  27011  lgamgulmlem5  27014  musum  27172  dchrptlem2  27246  dchrptlem3  27247  dchrpt  27248  lgsval  27282  lgsval4lem  27289  lgsneg  27302  lgsmod  27304  rpvmasum2  27493  padicfval  27597  ostth2  27618  ostth3  27619  ostth  27620  lmif  28871  islmib  28873  incistruhgr  29166  eucrct2eupth  30333  htthlem  31006  htth  31007  pjhfval  31485  hosmval  31824  hommval  31825  hodmval  31826  hfsmval  31827  hfmmval  31828  brafval  32032  kbfval  32041  mptprop  32790  indsn  32942  psgnfzto1st  33186  fxpsubm  33253  fxpsubg  33254  fxpsubrg  33255  elrgspnlem1  33323  elrgspnlem2  33324  elrgspnlem3  33325  elrgspnlem4  33326  elrgspn  33327  elrgspnsubrunlem1  33328  linds2eq  33464  elrspunidl  33511  elrspunsn  33512  evl1deg1  33659  evl1deg2  33660  evl1deg3  33661  mplasclco  33700  selvply1rhmlema  33702  selvply1rhmlemb  33703  selvply1rhmlem2  33705  selvply1rhmlem3  33706  selvply1rhmlem4  33707  selvply1rhmlem5  33708  selvply1rhm  33709  mplidom  33712  extvfval  33716  extvfv  33717  mvrvalind  33722  evlextv  33726  mplvrpmfgalem  33728  mplvrpmga  33729  mplvrpmmhm  33730  mplvrpmrhm  33731  psrgsum  33732  psrmonmul2  33735  psrmonprod  33736  splysubrg  33744  issply  33745  esplyval  33746  esplyfvaln  33758  vietalem  33763  vieta  33764  lbsdiflsp0  33810  fedgmullem1  33813  fedgmullem2  33814  fedgmul  33815  evls1fldgencl  33854  fldextrspunlsplem  33857  fldextrspunlsp  33858  extdgfialglem2  33877  mdetpmtr1  34007  zar0ring  34062  ordtcnvNEW  34104  ordtrest2NEW  34107  xrhval  34202  esum2dlem  34276  ofceq  34281  itgeq12dv  34510  ballotlemfval  34674  vtsval  34821  lpadval  34860  ptpconn  35461  cvmliftlem15  35526  cvmlift2lem4  35534  cvmlift2  35544  snmlval  35559  snmlflim  35560  satf  35581  mrsubfval  35736  mrsubrn  35741  elmsubrn  35756  msubrn  35757  msubco  35759  faclim  35974  faclim2  35976  prodeq12sdv  36446  itgeq12sdv  36447  cbvsumdavw  36507  cbvproddavw  36508  cbvsumdavw2  36523  cbvproddavw2  36524  knoppcnlem1  36799  knoppcnlem6  36804  knoppcnlem7  36805  bj-evaleq  37429  csbrdgg  37691  curfv  37967  matunitlindflem2  37984  poimirlem5  37992  poimirlem6  37993  poimirlem7  37994  poimirlem8  37995  poimirlem10  37997  poimirlem11  37998  poimirlem12  37999  poimirlem15  38002  poimirlem16  38003  poimirlem17  38004  poimirlem18  38005  poimirlem19  38006  poimirlem20  38007  poimirlem21  38008  poimirlem22  38009  poimirlem27  38014  voliunnfl  38031  itg2addnclem  38038  itg2addnclem3  38040  itg2addnc  38041  itg2gt0cn  38042  iblabsnclem  38050  iblmulc2nc  38052  ftc1anclem2  38061  ftc1anclem6  38065  ftc1anclem8  38067  ftc1anc  38068  ftc2nc  38069  upixp  38096  rrncmslem  38199  ismrer1  38205  tendoplcbv  41267  tendopl  41268  tendoicbv  41285  tendoi  41286  dihfval  41723  lcfl7N  41993  lcfrlem8  42041  lcfrlem9  42042  lcf1o  42043  hvmapval  42252  hdmap1fval  42288  hdmapffval  42318  hdmapfval  42319  hgmapffval  42377  hgmapfval  42378  lcmineqlem7  42520  lcmineqlem12  42525  aks6d1c6lem5  42662  rhmpsr  43033  evlsbagval  43036  evlselv  43039  fsuppind  43040  fsuppssindlem2  43042  fsuppssind  43043  mzpclval  43174  mzpcl2  43179  mzpexpmpt  43194  mzpsubst  43197  mzpcompact2lem  43200  rmxfval  43349  rmyfval  43350  aomclem8  43506  hbtlem1  43568  hbtlem7  43570  rfovfvd  44446  fsovrfovd  44453  fsovfvd  44454  fsovcnvlem  44457  dssmapfv2d  44462  dssmapnvod  44464  ntrneibex  44517  mnringmulrvald  44671  mnringmulrcld  44672  expgrowthi  44777  expgrowth  44779  binomcxplemdvsum  44799  addrval  44909  subrval  44910  mulvval  44911  fmulcl  46026  fmuldfeqlem1  46027  fprodcnlem  46044  fprodcn  46045  fnlimfv  46106  fnlimcnv  46110  fnlimfvre  46117  fnlimfvre2  46120  fnlimf  46121  fnlimabslt  46122  liminfval  46202  limsupresxr  46209  liminfresxr  46210  liminfvalxr  46226  fprodcncf  46343  dvnmptdivc  46381  dvnxpaek  46385  dvnmul  46386  dvmptfprod  46388  dvnprodlem1  46389  dvnprodlem2  46390  dvnprodlem3  46391  dvnprod  46392  stoweidlem2  46445  stoweidlem17  46460  stoweidlem19  46462  stoweidlem20  46463  stoweidlem43  46486  stoweidlem62  46505  stoweid  46506  dirkercncflem2  46547  fourierdlem112  46661  fourierdlem113  46662  etransclem1  46678  etransclem5  46682  etransclem17  46694  etransclem19  46696  etransclem22  46699  sge0val  46809  ovnlecvr  47001  ovncvrrp  47007  ovn0lem  47008  ovnsubaddlem1  47013  ovnsubadd  47015  hsphoif  47019  hsphoival  47022  hoidmv1lelem1  47034  hoidmv1lelem2  47035  hoidmv1lelem3  47036  hoidmv1le  47037  hoidmvlelem1  47038  hoidmvlelem2  47039  hoidmvlelem3  47040  hoidmvlelem4  47041  hoidmvlelem5  47042  hoidmvle  47043  ovnhoilem1  47044  ovnhoi  47046  hoidifhspval  47051  ovncvr2  47054  hoidifhspval2  47058  hspmbllem2  47070  hspmbllem3  47071  hspmbl  47072  ovnovollem1  47099  vonioolem2  47124  vonioo  47125  vonicclem2  47127  vonicc  47128  smflimlem4  47217  smflim  47220  smflim2  47249  smfsuplem2  47255  smfsup  47257  smfinf  47261  smflimsuplem2  47264  smflimsuplem5  47267  smflimsuplem7  47269  smflimsup  47271  cfsetsnfsetfo  47523  lincop  48899  1arymaptfv  49131  itcoval  49152  itcovalpc  49163  itcovalt2  49168  ackvalsuc1mpt  49169  ackval1  49172  fuco21  49826  prcofval  49868  aacllem  50291