Theorem mpteq2dv 5154

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

Syntax hints:   → wi 4   = wceq 1533   ∈ wcel 2110   ↦ cmpt 5138

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-ral 3143  df-opab 5121  df-mpt 5139

This theorem is referenced by:  ofeq  7405  mpocurryvald  7930  rdgeq1  8041  rdgeq2  8042  omv  8131  oev  8133  oieq1  8970  oieq2  8971  cantnflem1  9146  wunex2  10154  wuncval2  10163  rpnnen1  12376  seqof2  13422  relexpsucnnr  14378  relexp1g  14379  limsupval  14825  sumeq2w  15043  sumeq2ii  15044  cbvsum  15046  summo  15068  fsum  15071  fsumrlim  15160  fsumo1  15161  prodeq2w  15260  prodmo  15284  fprod  15289  bpolylem  15396  rpnnen2lem1  15561  rpnnen2lem2  15562  1arithlem1  16253  vdwapval  16303  vdwlem6  16316  vdwlem8  16318  vdwlem9  16319  vdwlem10  16320  ramub1lem2  16357  ramcl  16359  sloteq  16482  prdsplusgval  16740  prdsmulrval  16742  prdsdsval  16745  prdsvscaval  16746  ismon  16997  fucco  17226  curf1  17469  curf2  17473  yonedalem4a  17519  smndex1gbas  18061  smndex1gid  18062  grplactfval  18194  galactghm  18526  pmtrval  18573  sylow1  18722  sylow2b  18742  sylow3lem5  18750  sylow3  18752  iscyg  18992  gsumzaddlem  19035  gsumzmhm  19051  ablfac2  19205  gsumdixp  19353  fczpsrbag  20141  psrmulfval  20159  mvrval  20195  subrgmvr  20236  mplcoe1  20240  mplcoe3  20241  mplcoe5  20243  mplmon2  20267  subrgascl  20272  evlslem2  20286  evlslem3  20287  evlslem1  20289  mpfrcl  20292  evlsval  20293  evlsvar  20297  mpfind  20314  selvfval  20324  selvval  20325  mhpfval  20326  coe1fval  20367  pf1ind  20512  evl1gsumadd  20515  zncyg  20689  phllmhm  20770  isphld  20792  frlmgsum  20910  frlmipval  20917  frlmphl  20919  uvcval  20923  mamuval  20991  mamufv  20992  matgsum  21040  madetsumid  21064  mat1dimmul  21079  mvmulval  21146  mvmulfv  21147  mavmulfv  21149  1mavmul  21151  marepvval0  21169  mulmarep1gsum1  21176  mdetleib  21190  mdetleib2  21191  mdetfval1  21193  mdetleib1  21194  mdet0pr  21195  m1detdiag  21200  mdetralt  21211  mdetunilem9  21223  m2detleib  21234  smadiadetlem3  21271  mat2pmatmul  21333  decpmatmul  21374  decpmatmulsumfsupp  21375  pmatcollpw1  21378  monmatcollpw  21381  pmatcollpw3lem  21385  pmatcollpw3fi1lem2  21389  pm2mpval  21397  pm2mpfval  21398  mply1topmatval  21406  mp2pm2mplem1  21408  mp2pm2mplem3  21410  ptbasfi  22183  ptcnplem  22223  ptrescn  22241  cnmpt2k  22290  xkohmeo  22417  fmval  22545  fmf  22547  ptcmpg  22659  tmdmulg  22694  prdstmdd  22726  tsmspropd  22734  prdsxmslem2  23133  metdsval  23449  fsumcn  23472  expcn  23474  lebnumlem3  23561  pcoval  23609  pi1xfrcnv  23655  cphsscph  23848  rrxds  23990  rrxmval  24002  itg11  24286  mbfi1fseqlem2  24311  mbfi1fseqlem6  24315  mbfi1fseq  24316  mbfi1flimlem  24317  mbfmullem  24320  itg2const  24335  itg2mulc  24342  itg2monolem1  24345  itg2i1fseqle  24349  itg2i1fseq  24350  itg2addlem  24353  itg2cnlem1  24356  itg2cn  24358  isibl  24360  isibl2  24361  iblitg  24363  itgz  24375  itgvallem  24379  itgvallem3  24380  iblcnlem1  24382  itgcnlem  24384  iblrelem  24385  iblposlem  24386  iblpos  24387  itgrevallem1  24389  itgposval  24390  iblss2  24400  itgss  24406  itgfsum  24421  iblabslem  24422  iblmulc2  24425  bddmulibl  24433  itgcn  24437  ellimc  24465  dvnfval  24513  cpnfval  24523  dvexp  24544  dvexp2  24545  dvmptfsum  24566  dvlipcn  24585  dvivthlem1  24599  dvfsumle  24612  dvfsumabs  24614  dvfsumlem2  24618  elply2  24780  elplyr  24785  elplyd  24786  coeeu  24809  coelem  24810  coeeq  24811  plyco  24825  coe11  24837  coe1termlem  24842  dgrcolem1  24857  dvply2g  24868  elqaalem3  24904  eltayl  24942  tayl0  24944  taylthlem1  24955  taylthlem2  24956  ulmcau  24977  ulmdvlem1  24982  ulmdvlem3  24984  mtest  24986  mtestbdd  24987  pserval  24992  pserulm  25004  psercn  25008  pserdvlem2  25010  abelthlem3  25015  logtayl  25237  dvcxp1  25315  dvcncxp1  25318  logbmpt  25360  dmarea  25529  lgamgulmlem2  25601  lgamgulmlem5  25604  musum  25762  dchrptlem2  25835  dchrptlem3  25836  dchrpt  25837  lgsval  25871  lgsval4lem  25878  lgsneg  25891  lgsmod  25893  rpvmasum2  26082  padicfval  26186  ostth2  26207  ostth3  26208  ostth  26209  lmif  26565  islmib  26567  incistruhgr  26858  eucrct2eupth  28018  htthlem  28688  htth  28689  pjhfval  29167  hosmval  29506  hommval  29507  hodmval  29508  hfsmval  29509  hfmmval  29510  brafval  29714  kbfval  29723  mptprop  30428  psgnfzto1st  30742  linds2eq  30936  lbsdiflsp0  31017  fedgmullem1  31020  fedgmullem2  31021  fedgmul  31022  mdetpmtr1  31083  ordtcnvNEW  31158  ordtrest2NEW  31161  xrhval  31254  indval  31267  esum2dlem  31346  ofceq  31351  itgeq12dv  31579  ballotlemfval  31742  vtsval  31903  lpadval  31942  ptpconn  32475  cvmliftlem15  32540  cvmlift2lem4  32548  cvmlift2  32558  snmlval  32573  snmlflim  32574  satf  32595  mrsubfval  32750  mrsubrn  32755  elmsubrn  32770  msubrn  32771  msubco  32773  faclim  32973  faclim2  32975  trpredeq1  33054  trpredeq2  33055  knoppcnlem1  33827  knoppcnlem6  33832  knoppcnlem7  33833  bj-evaleq  34357  csbrdgg  34604  curfv  34866  matunitlindflem2  34883  poimirlem5  34891  poimirlem6  34892  poimirlem7  34893  poimirlem8  34894  poimirlem10  34896  poimirlem11  34897  poimirlem12  34898  poimirlem15  34901  poimirlem16  34902  poimirlem17  34903  poimirlem18  34904  poimirlem19  34905  poimirlem20  34906  poimirlem21  34907  poimirlem22  34908  poimirlem27  34913  voliunnfl  34930  itg2addnclem  34937  itg2addnclem3  34939  itg2addnc  34940  itg2gt0cn  34941  iblabsnclem  34949  iblmulc2nc  34951  ftc1anclem2  34962  ftc1anclem6  34966  ftc1anclem8  34968  ftc1anc  34969  ftc2nc  34970  upixp  34998  rrncmslem  35104  ismrer1  35110  tendoplcbv  37905  tendopl  37906  tendoicbv  37923  tendoi  37924  dihfval  38361  lcfl7N  38631  lcfrlem8  38679  lcfrlem9  38680  lcf1o  38681  hvmapval  38890  hdmap1fval  38926  hdmapffval  38956  hdmapfval  38957  hgmapffval  39015  hgmapfval  39016  mzpclval  39315  mzpcl2  39320  mzpexpmpt  39335  mzpsubst  39338  mzpcompact2lem  39341  rmxfval  39494  rmyfval  39495  aomclem8  39654  hbtlem1  39716  hbtlem7  39718  itgpowd  39814  rfovfvd  40341  fsovrfovd  40348  fsovfvd  40349  fsovcnvlem  40352  dssmapfv2d  40357  dssmapnvod  40359  ntrneibex  40416  expgrowthi  40658  expgrowth  40660  binomcxplemdvsum  40680  addrval  40791  subrval  40792  mulvval  40793  fmulcl  41855  fmuldfeqlem1  41856  fprodcnlem  41873  fprodcn  41874  fnlimfv  41937  fnlimcnv  41941  fnlimfvre  41948  fnlimfvre2  41951  fnlimf  41952  fnlimabslt  41953  liminfval  42033  limsupresxr  42040  liminfresxr  42041  liminfvalxr  42057  fprodcncf  42177  dvnmptdivc  42216  dvnxpaek  42220  dvnmul  42221  dvmptfprod  42223  dvnprodlem1  42224  dvnprodlem2  42225  dvnprodlem3  42226  dvnprod  42227  stoweidlem2  42281  stoweidlem17  42296  stoweidlem19  42298  stoweidlem20  42299  stoweidlem43  42322  stoweidlem62  42341  stoweid  42342  dirkercncflem2  42383  fourierdlem112  42497  fourierdlem113  42498  etransclem1  42514  etransclem5  42518  etransclem17  42530  etransclem19  42532  etransclem22  42535  sge0val  42642  ovnlecvr  42834  ovncvrrp  42840  ovn0lem  42841  ovnsubaddlem1  42846  ovnsubadd  42848  hsphoif  42852  hsphoival  42855  hoidmv1lelem1  42867  hoidmv1lelem2  42868  hoidmv1lelem3  42869  hoidmv1le  42870  hoidmvlelem1  42871  hoidmvlelem2  42872  hoidmvlelem3  42873  hoidmvlelem4  42874  hoidmvlelem5  42875  hoidmvle  42876  ovnhoilem1  42877  ovnhoi  42879  hoidifhspval  42884  ovncvr2  42887  hoidifhspval2  42891  hspmbllem2  42903  hspmbllem3  42904  hspmbl  42905  ovnovollem1  42932  vonioolem2  42957  vonioo  42958  vonicclem2  42960  vonicc  42961  smflimlem4  43044  smflim  43047  smflim2  43074  smfsuplem2  43080  smfsup  43082  smfinf  43086  smflimsuplem2  43089  smflimsuplem5  43092  smflimsuplem7  43094  smflimsup  43096  c0rhm  44177  c0rnghm  44178  lincop  44457  aacllem  44896