Theorem mpteq2dv 5199

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145   ↦ cmpt 5186

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-opab 5168  df-mpt 5187

This theorem is used by:  ifmpt2v  7515  ofeqd  7680  mpocurryvald  8268  rdgeq1  8400  rdgeq2  8401  omv  8499  oev  8501  curfv  8871  oieq1  9484  oieq2  9485  cantnflem1  9668  wunex2  10747  wuncval2  10756  indval  12245  rpnnen1  13033  seqof2  14124  relexpsucnnr  15098  relexp1g  15099  limsupval  15561  sumeq2w  15779  sumeq2ii  15780  cbvsum  15782  cbvsumv  15783  sumeq2sdv  15790  summo  15803  fsum  15806  fsumrlim  15898  fsumo1  15899  prodeq1  15996  prodeq2w  15999  prodeq2sdv  16011  prodmo  16023  fprod  16028  bpolylem  16134  rpnnen2lem1  16302  rpnnen2lem2  16303  1arithlem1  17015  vdwapval  17065  vdwlem6  17078  vdwlem8  17080  vdwlem9  17081  vdwlem10  17082  ramub1lem2  17119  ramcl  17121  sloteq  17275  prdsplusgval  17558  prdsmulrval  17560  prdsdsval  17563  prdsvscaval  17564  ismon  17822  fucco  18054  curf1  18313  curf2  18317  yonedalem4a  18363  smndex1gbas  19011  smndex1gbasOLD  19012  smndex1gid  19013  smndex1gidOLD  19014  smndex1igid  19015  grplactfval  19164  galactghm  19531  pmtrval  19578  sylow1  19730  sylow2b  19750  sylow3lem5  19758  sylow3  19760  iscyg  20006  gsumzaddlem  20048  gsumzmhm  20064  ablfac2  20218  gsumdixp  20459  c0rhm  20696  c0rnghm  20697  zncyg  21761  phllmhm  21845  isphld  21867  frlmgsum  21985  frlmipval  21992  frlmphl  21994  uvcval  21998  fczpsrbag  22136  psrmulfval  22158  psrascl  22193  mvrval  22196  subrgmvr  22249  mplcoe1  22253  mplcoe3  22254  mplcoe5  22256  mplmon2  22277  subrgascl  22282  evlslem2  22295  evlslem3  22296  evlslem1  22298  mpfrcl  22301  evlsval  22302  evlsvval  22306  evlsvvval  22309  evlsvar  22311  mpfind  22331  selvfval  22335  selvval  22336  selvvvval  22358  mhpfval  22366  psdfval  22386  psdval  22387  psdmvr  22397  coe1fval  22430  pf1ind  22580  evl1gsumadd  22583  rhmmpl  22605  rhmply1vr1  22609  mamuval  22615  mamufv  22616  matgsum  22659  madetsumid  22683  mat1dimmul  22698  mvmulval  22765  mvmulfv  22766  mavmulfv  22768  1mavmul  22770  marepvval0  22788  mulmarep1gsum1  22795  mdetleib  22809  mdetleib2  22810  mdetfval1  22812  mdetleib1  22813  mdet0pr  22814  m1detdiag  22819  mdetralt  22830  mdetunilem9  22842  m2detleib  22853  smadiadetlem3  22890  matunitlindflem2  22902  mat2pmatmul  22956  decpmatmul  22997  decpmatmulsumfsupp  22998  pmatcollpw1  23001  monmatcollpw  23004  pmatcollpw3lem  23008  pmatcollpw3fi1lem2  23012  pm2mpval  23020  pm2mpfval  23021  mply1topmatval  23029  mp2pm2mplem1  23031  mp2pm2mplem3  23033  ptbasfi  23807  ptcnplem  23847  ptrescn  23865  cnmpt2k  23914  xkohmeo  24041  fmval  24169  fmf  24171  ptcmpg  24283  tmdmulg  24318  prdstmdd  24350  tsmspropd  24358  prdsxmslem2  24755  metdsval  25074  fsumcn  25098  expcn  25100  lebnumlem3  25191  pcoval  25239  pi1xfrcnv  25285  cphsscph  25479  rrxds  25621  rrxmval  25633  itg11  25919  mbfi1fseqlem2  25944  mbfi1fseqlem6  25948  mbfi1fseq  25949  mbfi1flimlem  25950  mbfmullem  25953  itg2const  25968  itg2mulc  25975  itg2monolem1  25978  itg2i1fseqle  25982  itg2i1fseq  25983  itg2addlem  25986  itg2cnlem1  25989  itg2cn  25991  isibl  25993  isibl2  25994  iblitg  25996  itgeq1  26000  itgz  26008  itgvallem  26012  itgvallem3  26013  iblcnlem1  26015  itgcnlem  26017  iblrelem  26018  iblposlem  26019  iblpos  26020  itgrevallem1  26022  itgposval  26023  iblss2  26033  itgss  26039  itgfsum  26054  iblabslem  26055  iblmulc2  26058  bddmulibl  26066  itgcn  26072  ellimc  26100  dvnfval  26149  cpnfval  26159  dvexp  26180  dvexp2  26181  dvmptfsum  26202  dvlipcn  26221  dvivthlem1  26235  dvfsumle  26248  dvfsumabs  26250  dvfsumlem2  26254  itgpowd  26277  elply2  26421  elplyr  26426  elplyd  26427  coeeu  26451  coelem  26452  coeeq  26453  plyco  26467  coe11  26479  coe1termlem  26484  dgrcolem1  26499  dvply2g  26515  elqaalem3  26553  eltayl  26596  tayl0  26598  taylthlem1  26609  taylthlem2  26610  ulmcau  26631  ulmdvlem1  26636  ulmdvlem3  26638  mtest  26640  mtestbdd  26641  pserval  26646  pserulm  26658  psercn  26662  pserdvlem2  26664  abelthlem3  26669  logtayl  26897  dvcxp1  26977  dvcncxp1  26980  logbmpt  27025  dmarea  27194  lgamgulmlem2  27266  lgamgulmlem5  27269  musum  27427  dchrptlem2  27501  dchrptlem3  27502  dchrpt  27503  lgsval  27537  lgsval4lem  27544  lgsneg  27557  lgsmod  27559  rpvmasum2  27748  padicfval  27852  ostth2  27873  ostth3  27874  ostth  27875  lmif  29169  islmib  29171  incistruhgr  29536  eucrct2eupth  30725  htthlem  31398  htth  31399  pjhfval  31877  hosmval  32216  hommval  32217  hodmval  32218  hfsmval  32219  hfmmval  32220  brafval  32424  kbfval  32433  mptprop  33170  indsn  33309  psgnfzto1st  33545  fxpsubm  33612  fxpsubg  33613  fxpsubrg  33614  elrgspnlem1  33682  elrgspnlem2  33683  elrgspnlem3  33684  elrgspnlem4  33685  elrgspn  33686  elrgspnsubrunlem1  33687  linds2eq  33814  elrspunidl  33856  elrspunsn  33857  evl1deg1  33986  evl1deg2  33987  evl1deg3  33988  mplasclco  34026  selvply1rhmlema  34028  selvply1rhmlemb  34029  selvply1rhmlem2  34031  selvply1rhmlem3  34032  selvply1rhmlem4  34033  selvply1rhmlem5  34034  selvply1rhm  34035  mplidom  34038  extvfval  34042  extvfv  34043  mvrvalind  34048  evlextv  34052  mplvrpmfgalem  34054  mplvrpmga  34055  mplvrpmmhm  34056  mplvrpmrhm  34057  psrgsum  34058  psrmonmul2  34061  psrmonprod  34062  splysubrg  34070  issply  34071  esplyval  34072  esplyfvaln  34084  vietalem  34089  vieta  34090  lbsdiflsp0  34136  fedgmullem1  34139  fedgmullem2  34140  fedgmul  34141  evls1fldgencl  34180  fldextrspunlsplem  34183  fldextrspunlsp  34184  extdgfialglem2  34203  mdetpmtr1  34333  zar0ring  34388  ordtcnvNEW  34430  ordtrest2NEW  34433  xrhval  34528  esum2dlem  34602  ofceq  34607  itgeq12dv  34837  ballotlemfval  35001  vtsval  35145  lpadval  35187  ptpconn  35812  cvmliftlem15  35877  cvmlift2lem4  35885  cvmlift2  35895  snmlval  35910  snmlflim  35911  satf  35932  mrsubfval  36087  mrsubrn  36092  elmsubrn  36107  msubrn  36108  msubco  36110  faclim  36325  faclim2  36327  prodeq12sdv  36838  itgeq12sdv  36839  cbvsumdavw  36899  cbvproddavw  36900  cbvsumdavw2  36915  cbvproddavw2  36916  knoppcnlem1  37190  knoppcnlem6  37195  knoppcnlem7  37196  bj-evaleq  37821  csbrdgg  38083  poimirlem5  38374  poimirlem6  38375  poimirlem7  38376  poimirlem8  38377  poimirlem10  38379  poimirlem11  38380  poimirlem12  38381  poimirlem15  38384  poimirlem16  38385  poimirlem17  38386  poimirlem18  38387  poimirlem19  38388  poimirlem20  38389  poimirlem21  38390  poimirlem22  38391  poimirlem27  38396  voliunnfl  38413  itg2addnclem  38420  itg2addnclem3  38422  itg2addnc  38423  itg2gt0cn  38424  iblabsnclem  38432  iblmulc2nc  38434  ftc1anclem2  38443  ftc1anclem6  38447  ftc1anclem8  38449  ftc1anc  38450  ftc2nc  38451  upixp  38479  rrncmslem  38582  ismrer1  38588  tendoplcbv  41648  tendopl  41649  tendoicbv  41666  tendoi  41667  dihfval  42104  lcfl7N  42374  lcfrlem8  42422  lcfrlem9  42423  lcf1o  42424  hvmapval  42633  hdmap1fval  42669  hdmapffval  42699  hdmapfval  42700  hgmapffval  42758  hgmapfval  42759  lcmineqlem7  42901  lcmineqlem12  42906  aks6d1c6lem5  43043  rhmpsr  43429  evlsbagval  43432  evlselv  43435  fsuppind  43436  fsuppssindlem2  43438  fsuppssind  43439  mzpclval  43570  mzpcl2  43575  mzpexpmpt  43590  mzpsubst  43593  mzpcompact2lem  43596  rmxfval  43745  rmyfval  43746  aomclem8  43902  hbtlem1  43964  hbtlem7  43966  rfovfvd  44842  fsovrfovd  44849  fsovfvd  44850  fsovcnvlem  44853  dssmapfv2d  44858  dssmapnvod  44860  ntrneibex  44913  mnringmulrvald  45065  mnringmulrcld  45066  expgrowthi  45157  expgrowth  45159  binomcxplemdvsum  45179  addrval  45288  subrval  45289  mulvval  45290  fmulcl  46411  fmuldfeqlem1  46412  fprodcnlem  46429  fprodcn  46430  fnlimfv  46491  fnlimcnv  46495  fnlimfvre  46502  fnlimfvre2  46505  fnlimf  46506  fnlimabslt  46507  liminfval  46587  limsupresxr  46594  liminfresxr  46595  liminfvalxr  46611  fprodcncf  46728  dvnmptdivc  46766  dvnxpaek  46770  dvnmul  46771  dvmptfprod  46773  dvnprodlem1  46774  dvnprodlem2  46775  dvnprodlem3  46776  dvnprod  46777  stoweidlem2  46830  stoweidlem17  46845  stoweidlem19  46847  stoweidlem20  46848  stoweidlem43  46871  stoweidlem62  46890  stoweid  46891  dirkercncflem2  46932  fourierdlem112  47046  fourierdlem113  47047  etransclem1  47063  etransclem5  47067  etransclem17  47079  etransclem19  47081  etransclem22  47084  sge0val  47194  ovnlecvr  47386  ovncvrrp  47392  ovn0lem  47393  ovnsubaddlem1  47398  ovnsubadd  47400  hsphoif  47404  hsphoival  47407  hoidmv1lelem1  47419  hoidmv1lelem2  47420  hoidmv1lelem3  47421  hoidmv1le  47422  hoidmvlelem1  47423  hoidmvlelem2  47424  hoidmvlelem3  47425  hoidmvlelem4  47426  hoidmvlelem5  47427  hoidmvle  47428  ovnhoilem1  47429  ovnhoi  47431  hoidifhspval  47436  ovncvr2  47439  hoidifhspval2  47443  hspmbllem2  47455  hspmbllem3  47456  hspmbl  47457  ovnovollem1  47484  vonioolem2  47509  vonioo  47510  vonicclem2  47512  vonicc  47513  smflimlem4  47602  smflim  47605  smflim2  47634  smfsuplem2  47640  smfsup  47642  smfinf  47646  smflimsuplem2  47649  smflimsuplem5  47652  smflimsuplem7  47654  smflimsup  47656  cfsetsnfsetfo  47948  lincop  49338  1arymaptfv  49570  itcoval  49591  itcovalpc  49602  itcovalt2  49607  ackvalsuc1mpt  49608  ackval1  49611  fuco21  50262  prcofval  50304  aacllem  50772  crosspval  50787  crosspdot0lem  50796  veronesevald  50804  veronesematrowexpd  50815