Theorem mpteq2dv 5020

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

Syntax hints:   → wi 4   = wceq 1508   ∈ wcel 2051   ↦ cmpt 5005

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-12 2107  ax-ext 2745

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-clab 2754  df-cleq 2766  df-clel 2841  df-ral 3088  df-opab 4989  df-mpt 5006

This theorem is referenced by:  ofeq  7228  mpocurryvald  7738  rdgeq1  7850  rdgeq2  7851  omv  7938  oev  7940  oieq1  8770  oieq2  8771  cantnflem1  8945  wunex2  9957  wuncval2  9966  rpnnen1  12196  seqof2  13242  relexpsucnnr  14244  relexp1g  14245  limsupval  14691  sumeq2w  14908  sumeq2ii  14909  cbvsum  14911  summo  14933  fsum  14936  fsumrlim  15025  fsumo1  15026  prodeq2w  15125  prodmo  15149  fprod  15154  bpolylem  15261  rpnnen2lem1  15426  rpnnen2lem2  15427  1arithlem1  16114  vdwapval  16164  vdwlem6  16177  vdwlem8  16179  vdwlem9  16180  vdwlem10  16181  ramub1lem2  16218  ramcl  16220  sloteq  16343  prdsplusgval  16601  prdsmulrval  16603  prdsdsval  16606  prdsvscaval  16607  ismon  16874  fucco  17103  curf1  17346  curf2  17350  yonedalem4a  17396  grplactfval  18000  galactghm  18305  pmtrval  18353  sylow1  18502  sylow2b  18522  sylow3lem5  18530  sylow3  18532  iscyg  18767  gsumzaddlem  18807  gsumzmhm  18823  ablfac2  18974  gsumdixp  19095  fczpsrbag  19874  psrmulfval  19892  mvrval  19928  subrgmvr  19968  mplcoe1  19972  mplcoe3  19973  mplcoe5  19975  mplmon2  19999  subrgascl  20004  evlslem2  20018  evlslem3  20020  evlslem1  20021  mpfrcl  20024  evlsval  20025  evlsvar  20029  mpfind  20042  mhpfval  20051  coe1fval  20092  pf1ind  20236  evl1gsumadd  20239  zncyg  20413  phllmhm  20494  isphld  20516  frlmgsum  20634  frlmipval  20641  frlmphl  20643  uvcval  20647  mamuval  20715  mamufv  20716  matgsum  20766  madetsumid  20790  mat1dimmul  20805  mvmulval  20872  mvmulfv  20873  mavmulfv  20875  1mavmul  20877  marepvval0  20895  mulmarep1gsum1  20902  mdetleib  20916  mdetleib2  20917  mdetfval1  20919  mdetleib1  20920  mdet0pr  20921  m1detdiag  20926  mdetralt  20937  mdetunilem9  20949  m2detleib  20960  smadiadetlem3  20997  mat2pmatmul  21059  decpmatmul  21100  decpmatmulsumfsupp  21101  pmatcollpw1  21104  monmatcollpw  21107  pmatcollpw3lem  21111  pmatcollpw3fi1lem2  21115  pm2mpval  21123  pm2mpfval  21124  mply1topmatval  21132  mp2pm2mplem1  21134  mp2pm2mplem3  21136  ptbasfi  21909  ptcnplem  21949  ptrescn  21967  cnmpt2k  22016  xkohmeo  22143  fmval  22271  fmf  22273  ptcmpg  22385  tmdmulg  22420  prdstmdd  22451  tsmspropd  22459  prdsxmslem2  22858  metdsval  23174  fsumcn  23197  expcn  23199  lebnumlem3  23286  pcoval  23334  pi1xfrcnv  23380  cphsscph  23573  rrxds  23715  rrxmval  23727  itg11  24011  mbfi1fseqlem2  24036  mbfi1fseqlem6  24040  mbfi1fseq  24041  mbfi1flimlem  24042  mbfmullem  24045  itg2const  24060  itg2mulc  24067  itg2monolem1  24070  itg2i1fseqle  24074  itg2i1fseq  24075  itg2addlem  24078  itg2cnlem1  24081  itg2cn  24083  isibl  24085  isibl2  24086  iblitg  24088  itgz  24100  itgvallem  24104  itgvallem3  24105  iblcnlem1  24107  itgcnlem  24109  iblrelem  24110  iblposlem  24111  iblpos  24112  itgrevallem1  24114  itgposval  24115  iblss2  24125  itgss  24131  itgfsum  24146  iblabslem  24147  iblmulc2  24150  bddmulibl  24158  itgcn  24162  ellimc  24190  dvnfval  24238  cpnfval  24248  dvexp  24269  dvexp2  24270  dvmptfsum  24291  dvlipcn  24310  dvivthlem1  24324  dvfsumle  24337  dvfsumabs  24339  dvfsumlem2  24343  elply2  24505  elplyr  24510  elplyd  24511  coeeu  24534  coelem  24535  coeeq  24536  plyco  24550  coe11  24562  coe1termlem  24567  dgrcolem1  24582  dvply2g  24593  elqaalem3  24629  eltayl  24667  tayl0  24669  taylthlem1  24680  taylthlem2  24681  ulmcau  24702  ulmdvlem1  24707  ulmdvlem3  24709  mtest  24711  mtestbdd  24712  pserval  24717  pserulm  24729  psercn  24733  pserdvlem2  24735  abelthlem3  24740  logtayl  24960  dvcxp1  25038  dvcncxp1  25041  logbmpt  25083  dmarea  25253  lgamgulmlem2  25325  lgamgulmlem5  25328  musum  25486  dchrptlem2  25559  dchrptlem3  25560  dchrpt  25561  lgsval  25595  lgsval4lem  25602  lgsneg  25615  lgsmod  25617  rpvmasum2  25806  padicfval  25910  ostth2  25931  ostth3  25932  ostth  25933  lmif  26289  islmib  26291  incistruhgr  26583  eucrct2eupthOLD  27792  eucrct2eupth  27793  htthlem  28489  htth  28490  pjhfval  28970  hosmval  29309  hommval  29310  hodmval  29311  hfsmval  29312  hfmmval  29313  brafval  29517  kbfval  29526  mptprop  30211  linds2eq  30645  lbsdiflsp0  30684  fedgmullem1  30687  fedgmullem2  30688  fedgmul  30689  psgnfzto1st  30729  mdetpmtr1  30763  ordtcnvNEW  30840  ordtrest2NEW  30843  xrhval  30936  indval  30949  esum2dlem  31028  ofceq  31033  itgeq12dv  31262  ballotlemfval  31426  vtsval  31589  lpadval  31628  ptpconn  32098  cvmliftlem15  32163  cvmlift2lem4  32171  cvmlift2  32181  snmlval  32196  snmlflim  32197  satf  32214  mrsubfval  32308  mrsubrn  32313  elmsubrn  32328  msubrn  32329  msubco  32331  faclim  32531  faclim2  32533  trpredeq1  32613  trpredeq2  32614  knoppcnlem1  33385  knoppcnlem6  33390  knoppcnlem7  33391  bj-evaleq  33905  csbrdgg  34085  curfv  34346  matunitlindflem2  34363  poimirlem5  34371  poimirlem6  34372  poimirlem7  34373  poimirlem8  34374  poimirlem10  34376  poimirlem11  34377  poimirlem12  34378  poimirlem15  34381  poimirlem16  34382  poimirlem17  34383  poimirlem18  34384  poimirlem19  34385  poimirlem20  34386  poimirlem21  34387  poimirlem22  34388  poimirlem27  34393  voliunnfl  34410  itg2addnclem  34417  itg2addnclem3  34419  itg2addnc  34420  itg2gt0cn  34421  iblabsnclem  34429  iblmulc2nc  34431  ftc1anclem2  34442  ftc1anclem6  34446  ftc1anclem8  34448  ftc1anc  34449  ftc2nc  34450  upixp  34479  rrncmslem  34585  ismrer1  34591  tendoplcbv  37389  tendopl  37390  tendoicbv  37407  tendoi  37408  dihfval  37845  lcfl7N  38115  lcfrlem8  38163  lcfrlem9  38164  lcf1o  38165  hvmapval  38374  hdmap1fval  38410  hdmapffval  38440  hdmapfval  38441  hgmapffval  38499  hgmapfval  38500  mzpclval  38751  mzpcl2  38756  mzpexpmpt  38771  mzpsubst  38774  mzpcompact2lem  38777  rmxfval  38931  rmyfval  38932  aomclem8  39091  hbtlem1  39153  hbtlem7  39155  itgpowd  39251  rfovfvd  39745  fsovrfovd  39752  fsovfvd  39753  fsovcnvlem  39756  dssmapfv2d  39761  dssmapnvod  39763  ntrneibex  39820  expgrowthi  40115  expgrowth  40117  binomcxplemdvsum  40137  addrval  40251  subrval  40252  mulvval  40253  fmulcl  41323  fmuldfeqlem1  41324  fprodcnlem  41341  fprodcn  41342  fnlimfv  41405  fnlimcnv  41409  fnlimfvre  41416  fnlimfvre2  41419  fnlimf  41420  fnlimabslt  41421  liminfval  41501  limsupresxr  41508  liminfresxr  41509  liminfvalxr  41525  fprodcncf  41644  dvnmptdivc  41683  dvnxpaek  41687  dvnmul  41688  dvmptfprod  41690  dvnprodlem1  41691  dvnprodlem2  41692  dvnprodlem3  41693  dvnprod  41694  stoweidlem2  41748  stoweidlem17  41763  stoweidlem19  41765  stoweidlem20  41766  stoweidlem43  41789  stoweidlem62  41808  stoweid  41809  dirkercncflem2  41850  fourierdlem112  41964  fourierdlem113  41965  etransclem1  41981  etransclem5  41985  etransclem17  41997  etransclem19  41999  etransclem22  42002  sge0val  42109  ovnlecvr  42301  ovncvrrp  42307  ovn0lem  42308  ovnsubaddlem1  42313  ovnsubadd  42315  hsphoif  42319  hsphoival  42322  hoidmv1lelem1  42334  hoidmv1lelem2  42335  hoidmv1lelem3  42336  hoidmv1le  42337  hoidmvlelem1  42338  hoidmvlelem2  42339  hoidmvlelem3  42340  hoidmvlelem4  42341  hoidmvlelem5  42342  hoidmvle  42343  ovnhoilem1  42344  ovnhoi  42346  hoidifhspval  42351  ovncvr2  42354  hoidifhspval2  42358  hspmbllem2  42370  hspmbllem3  42371  hspmbl  42372  ovnovollem1  42399  vonioolem2  42424  vonioo  42425  vonicclem2  42427  vonicc  42428  smflimlem4  42511  smflim  42514  smflim2  42541  smfsuplem2  42547  smfsup  42549  smfinf  42553  smflimsuplem2  42556  smflimsuplem5  42559  smflimsuplem7  42561  smflimsup  42563  c0rhm  43577  c0rnghm  43578  lincop  43860  aacllem  44299