Theorem mpteq2dv 5191

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

Syntax hints:   → wi 4   = wceq 1559   ∈ wcel 2141   ↦ cmpt 5178

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-opab 5160  df-mpt 5179

This theorem is referenced by:  ifmpt2v  7493  ofeqd  7657  mpocurryvald  8244  rdgeq1  8376  rdgeq2  8377  omv  8475  oev  8477  oieq1  9454  oieq2  9455  cantnflem1  9638  wunex2  10690  wuncval2  10699  indval  12192  rpnnen1  12978  seqof2  14067  relexpsucnnr  15032  relexp1g  15033  limsupval  15492  sumeq2w  15710  sumeq2ii  15711  cbvsum  15713  cbvsumv  15714  sumeq2sdv  15721  summo  15735  fsum  15738  fsumrlim  15830  fsumo1  15831  prodeq1  15928  prodeq2w  15931  prodeq2sdv  15944  prodmo  15957  fprod  15962  bpolylem  16069  rpnnen2lem1  16237  rpnnen2lem2  16238  1arithlem1  16950  vdwapval  17000  vdwlem6  17013  vdwlem8  17015  vdwlem9  17016  vdwlem10  17017  ramub1lem2  17054  ramcl  17056  sloteq  17210  prdsplusgval  17493  prdsmulrval  17495  prdsdsval  17498  prdsvscaval  17499  ismon  17757  fucco  17989  curf1  18248  curf2  18252  yonedalem4a  18298  smndex1gbas  18927  smndex1gbasOLD  18928  smndex1gid  18929  smndex1gidOLD  18930  smndex1igid  18931  grplactfval  19074  galactghm  19435  pmtrval  19482  sylow1  19634  sylow2b  19654  sylow3lem5  19662  sylow3  19664  iscyg  19910  gsumzaddlem  19952  gsumzmhm  19968  ablfac2  20122  gsumdixp  20354  c0rhm  20571  c0rnghm  20572  zncyg  21588  phllmhm  21672  isphld  21694  frlmgsum  21812  frlmipval  21819  frlmphl  21821  uvcval  21825  fczpsrbag  21961  psrmulfval  21983  psrascl  22018  mvrval  22021  subrgmvr  22074  mplcoe1  22078  mplcoe3  22079  mplcoe5  22081  mplmon2  22102  subrgascl  22107  evlslem2  22120  evlslem3  22121  evlslem1  22123  mpfrcl  22126  evlsval  22127  evlsvval  22131  evlsvvval  22134  evlsvar  22136  mpfind  22156  selvfval  22160  selvval  22161  selvvvval  22183  mhpfval  22191  psdfval  22211  psdval  22212  psdmvr  22222  coe1fval  22255  pf1ind  22406  evl1gsumadd  22409  rhmmpl  22431  rhmply1vr1  22435  mamuval  22441  mamufv  22442  matgsum  22485  madetsumid  22509  mat1dimmul  22524  mvmulval  22591  mvmulfv  22592  mavmulfv  22594  1mavmul  22596  marepvval0  22614  mulmarep1gsum1  22621  mdetleib  22635  mdetleib2  22636  mdetfval1  22638  mdetleib1  22639  mdet0pr  22640  m1detdiag  22645  mdetralt  22656  mdetunilem9  22668  m2detleib  22679  smadiadetlem3  22716  mat2pmatmul  22779  decpmatmul  22820  decpmatmulsumfsupp  22821  pmatcollpw1  22824  monmatcollpw  22827  pmatcollpw3lem  22831  pmatcollpw3fi1lem2  22835  pm2mpval  22843  pm2mpfval  22844  mply1topmatval  22852  mp2pm2mplem1  22854  mp2pm2mplem3  22856  ptbasfi  23629  ptcnplem  23669  ptrescn  23687  cnmpt2k  23736  xkohmeo  23863  fmval  23991  fmf  23993  ptcmpg  24105  tmdmulg  24140  prdstmdd  24172  tsmspropd  24180  prdsxmslem2  24577  metdsval  24896  fsumcn  24920  expcn  24922  lebnumlem3  25013  pcoval  25061  pi1xfrcnv  25107  cphsscph  25301  rrxds  25443  rrxmval  25455  itg11  25741  mbfi1fseqlem2  25766  mbfi1fseqlem6  25770  mbfi1fseq  25771  mbfi1flimlem  25772  mbfmullem  25775  itg2const  25790  itg2mulc  25797  itg2monolem1  25800  itg2i1fseqle  25804  itg2i1fseq  25805  itg2addlem  25808  itg2cnlem1  25811  itg2cn  25813  isibl  25815  isibl2  25816  iblitg  25818  itgeq1  25823  itgz  25831  itgvallem  25835  itgvallem3  25836  iblcnlem1  25838  itgcnlem  25840  iblrelem  25841  iblposlem  25842  iblpos  25843  itgrevallem1  25845  itgposval  25846  iblss2  25856  itgss  25862  itgfsum  25877  iblabslem  25878  iblmulc2  25881  bddmulibl  25889  itgcn  25895  ellimc  25923  dvnfval  25972  cpnfval  25982  dvexp  26003  dvexp2  26004  dvmptfsum  26025  dvlipcn  26044  dvivthlem1  26058  dvfsumle  26071  dvfsumabs  26073  dvfsumlem2  26077  itgpowd  26100  elply2  26244  elplyr  26249  elplyd  26250  coeeu  26273  coelem  26274  coeeq  26275  plyco  26289  coe11  26301  coe1termlem  26306  dgrcolem1  26321  dvply2g  26337  elqaalem3  26373  eltayl  26411  tayl0  26413  taylthlem1  26424  taylthlem2  26425  ulmcau  26446  ulmdvlem1  26451  ulmdvlem3  26453  mtest  26455  mtestbdd  26456  pserval  26461  pserulm  26473  psercn  26477  pserdvlem2  26479  abelthlem3  26484  logtayl  26713  dvcxp1  26793  dvcncxp1  26796  logbmpt  26841  dmarea  27010  lgamgulmlem2  27082  lgamgulmlem5  27085  musum  27243  dchrptlem2  27317  dchrptlem3  27318  dchrpt  27319  lgsval  27353  lgsval4lem  27360  lgsneg  27373  lgsmod  27375  rpvmasum2  27564  padicfval  27668  ostth2  27689  ostth3  27690  ostth  27691  lmif  28942  islmib  28944  incistruhgr  29237  eucrct2eupth  30404  htthlem  31077  htth  31078  pjhfval  31556  hosmval  31895  hommval  31896  hodmval  31897  hfsmval  31898  hfmmval  31899  brafval  32103  kbfval  32112  mptprop  32861  indsn  33002  psgnfzto1st  33246  fxpsubm  33313  fxpsubg  33314  fxpsubrg  33315  elrgspnlem1  33384  elrgspnlem2  33385  elrgspnlem3  33386  elrgspnlem4  33387  elrgspn  33388  elrgspnsubrunlem1  33389  linds2eq  33528  elrspunidl  33575  elrspunsn  33576  evl1deg1  33733  evl1deg2  33734  evl1deg3  33735  mplasclco  33774  selvply1rhmlema  33776  selvply1rhmlemb  33777  selvply1rhmlem2  33779  selvply1rhmlem3  33780  selvply1rhmlem4  33781  selvply1rhmlem5  33782  selvply1rhm  33783  mplidom  33786  extvfval  33790  extvfv  33791  mvrvalind  33796  evlextv  33800  mplvrpmfgalem  33802  mplvrpmga  33803  mplvrpmmhm  33804  mplvrpmrhm  33805  psrgsum  33806  psrmonmul2  33809  psrmonprod  33810  splysubrg  33818  issply  33819  esplyval  33820  esplyfvaln  33832  vietalem  33837  vieta  33838  lbsdiflsp0  33884  fedgmullem1  33887  fedgmullem2  33888  fedgmul  33889  evls1fldgencl  33928  fldextrspunlsplem  33931  fldextrspunlsp  33932  extdgfialglem2  33951  mdetpmtr1  34081  zar0ring  34136  ordtcnvNEW  34178  ordtrest2NEW  34181  xrhval  34276  esum2dlem  34350  ofceq  34355  itgeq12dv  34584  ballotlemfval  34748  vtsval  34892  lpadval  34934  ptpconn  35544  cvmliftlem15  35609  cvmlift2lem4  35617  cvmlift2  35627  snmlval  35642  snmlflim  35643  satf  35664  mrsubfval  35819  mrsubrn  35824  elmsubrn  35839  msubrn  35840  msubco  35842  faclim  36057  faclim2  36059  prodeq12sdv  36539  itgeq12sdv  36540  cbvsumdavw  36600  cbvproddavw  36601  cbvsumdavw2  36616  cbvproddavw2  36617  knoppcnlem1  36892  knoppcnlem6  36897  knoppcnlem7  36898  bj-evaleq  37522  csbrdgg  37784  curfv  38060  matunitlindflem2  38077  poimirlem5  38085  poimirlem6  38086  poimirlem7  38087  poimirlem8  38088  poimirlem10  38090  poimirlem11  38091  poimirlem12  38092  poimirlem15  38095  poimirlem16  38096  poimirlem17  38097  poimirlem18  38098  poimirlem19  38099  poimirlem20  38100  poimirlem21  38101  poimirlem22  38102  poimirlem27  38107  voliunnfl  38124  itg2addnclem  38131  itg2addnclem3  38133  itg2addnc  38134  itg2gt0cn  38135  iblabsnclem  38143  iblmulc2nc  38145  ftc1anclem2  38154  ftc1anclem6  38158  ftc1anclem8  38160  ftc1anc  38161  ftc2nc  38162  upixp  38189  rrncmslem  38292  ismrer1  38298  tendoplcbv  41360  tendopl  41361  tendoicbv  41378  tendoi  41379  dihfval  41816  lcfl7N  42086  lcfrlem8  42134  lcfrlem9  42135  lcf1o  42136  hvmapval  42345  hdmap1fval  42381  hdmapffval  42411  hdmapfval  42412  hgmapffval  42470  hgmapfval  42471  lcmineqlem7  42613  lcmineqlem12  42618  aks6d1c6lem5  42755  rhmpsr  43126  evlsbagval  43129  evlselv  43132  fsuppind  43133  fsuppssindlem2  43135  fsuppssind  43136  mzpclval  43267  mzpcl2  43272  mzpexpmpt  43287  mzpsubst  43290  mzpcompact2lem  43293  rmxfval  43442  rmyfval  43443  aomclem8  43599  hbtlem1  43661  hbtlem7  43663  rfovfvd  44539  fsovrfovd  44546  fsovfvd  44547  fsovcnvlem  44550  dssmapfv2d  44555  dssmapnvod  44557  ntrneibex  44610  mnringmulrvald  44764  mnringmulrcld  44765  expgrowthi  44870  expgrowth  44872  binomcxplemdvsum  44892  addrval  45002  subrval  45003  mulvval  45004  fmulcl  46118  fmuldfeqlem1  46119  fprodcnlem  46136  fprodcn  46137  fnlimfv  46198  fnlimcnv  46202  fnlimfvre  46209  fnlimfvre2  46212  fnlimf  46213  fnlimabslt  46214  liminfval  46294  limsupresxr  46301  liminfresxr  46302  liminfvalxr  46318  fprodcncf  46435  dvnmptdivc  46473  dvnxpaek  46477  dvnmul  46478  dvmptfprod  46480  dvnprodlem1  46481  dvnprodlem2  46482  dvnprodlem3  46483  dvnprod  46484  stoweidlem2  46537  stoweidlem17  46552  stoweidlem19  46554  stoweidlem20  46555  stoweidlem43  46578  stoweidlem62  46597  stoweid  46598  dirkercncflem2  46639  fourierdlem112  46753  fourierdlem113  46754  etransclem1  46770  etransclem5  46774  etransclem17  46786  etransclem19  46788  etransclem22  46791  sge0val  46901  ovnlecvr  47093  ovncvrrp  47099  ovn0lem  47100  ovnsubaddlem1  47105  ovnsubadd  47107  hsphoif  47111  hsphoival  47114  hoidmv1lelem1  47126  hoidmv1lelem2  47127  hoidmv1lelem3  47128  hoidmv1le  47129  hoidmvlelem1  47130  hoidmvlelem2  47131  hoidmvlelem3  47132  hoidmvlelem4  47133  hoidmvlelem5  47134  hoidmvle  47135  ovnhoilem1  47136  ovnhoi  47138  hoidifhspval  47143  ovncvr2  47146  hoidifhspval2  47150  hspmbllem2  47162  hspmbllem3  47163  hspmbl  47164  ovnovollem1  47191  vonioolem2  47216  vonioo  47217  vonicclem2  47219  vonicc  47220  smflimlem4  47309  smflim  47312  smflim2  47341  smfsuplem2  47347  smfsup  47349  smfinf  47353  smflimsuplem2  47356  smflimsuplem5  47359  smflimsuplem7  47361  smflimsup  47363  cfsetsnfsetfo  47615  lincop  48991  1arymaptfv  49223  itcoval  49244  itcovalpc  49255  itcovalt2  49260  ackvalsuc1mpt  49261  ackval1  49264  fuco21  49918  prcofval  49960  aacllem  50383