Theorem mpteq2dv 5205

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-opab 5174  df-mpt 5193

This theorem is used by:  ifmpt2v  7553  ofeqd  7727  mpocurryvald  8325  rdgeq1  8457  rdgeq2  8458  omv  8558  oev  8560  curfv  8930  oieq1  9543  oieq2  9544  cantnflem1  9727  wunex2  10862  wuncval2  10871  indval  12363  rpnnen1  13151  seqof2  14243  relexpsucnnr  15221  relexp1g  15222  limsupval  15685  sumeq2w  15903  sumeq2ii  15904  cbvsum  15906  cbvsumv  15907  sumeq2sdv  15914  summo  15927  fsum  15930  fsumrlim  16022  fsumo1  16023  prodeq1  16120  prodeq2w  16123  prodeq2sdv  16135  prodmo  16147  fprod  16152  bpolylem  16258  rpnnen2lem1  16426  rpnnen2lem2  16427  1arithlem1  17145  vdwapval  17195  vdwlem6  17208  vdwlem8  17210  vdwlem9  17211  vdwlem10  17212  ramub1lem2  17249  ramcl  17251  sloteq  17405  prdsplusgval  17694  prdsmulrval  17696  prdsdsval  17699  prdsvscaval  17700  ismon  17958  fucco  18190  curf1  18449  curf2  18453  yonedalem4a  18499  smndex1gbas  19148  smndex1gbasOLD  19149  smndex1gid  19150  smndex1gidOLD  19151  smndex1igid  19152  grplactfval  19301  galactghm  19669  pmtrval  19716  sylow1  19868  sylow2b  19888  sylow3lem5  19896  sylow3  19898  iscyg  20144  gsumzaddlem  20186  gsumzmhm  20202  ablfac2  20356  gsumdixp  20599  c0rhm  20837  c0rnghm  20838  zncyg  21909  phllmhm  21993  isphld  22015  frlmgsum  22133  frlmipval  22140  frlmphl  22142  uvcval  22146  fczpsrbag  22284  psrmulfval  22306  psrascl  22341  mvrval  22344  subrgmvr  22397  mplcoe1  22401  mplcoe3  22402  mplcoe5  22404  mplmon2  22425  subrgascl  22430  evlslem2  22443  evlslem3  22444  evlslem1  22446  mpfrcl  22449  evlsval  22450  evlsvval  22454  evlsvvval  22457  evlsvar  22459  mpfind  22479  selvfval  22483  selvval  22484  selvvvval  22506  mhpfval  22514  psdfval  22534  psdval  22535  psdmvr  22545  coe1fval  22578  pf1ind  22728  evl1gsumadd  22731  rhmmpl  22753  rhmply1vr1  22757  mamuval  22763  mamufv  22764  matgsum  22807  madetsumid  22831  mat1dimmul  22846  mvmulval  22913  mvmulfv  22914  mavmulfv  22916  1mavmul  22918  marepvval0  22936  mulmarep1gsum1  22943  mdetleib  22957  mdetleib2  22958  mdetfval1  22960  mdetleib1  22961  mdet0pr  22962  m1detdiag  22967  mdetralt  22978  mdetunilem9  22990  m2detleib  23001  smadiadetlem3  23038  matunitlindflem2  23050  mat2pmatmul  23104  decpmatmul  23145  decpmatmulsumfsupp  23146  pmatcollpw1  23149  monmatcollpw  23152  pmatcollpw3lem  23156  pmatcollpw3fi1lem2  23160  pm2mpval  23168  pm2mpfval  23169  mply1topmatval  23177  mp2pm2mplem1  23179  mp2pm2mplem3  23181  ptbasfi  23955  ptcnplem  23995  ptrescn  24013  cnmpt2k  24062  xkohmeo  24189  fmval  24317  fmf  24319  ptcmpg  24431  tmdmulg  24466  prdstmdd  24498  tsmspropd  24506  prdsxmslem2  24903  metdsval  25222  fsumcn  25246  expcn  25248  lebnumlem3  25339  pcoval  25387  pi1xfrcnv  25433  cphsscph  25627  rrxds  25769  rrxmval  25781  itg11  26067  mbfi1fseqlem2  26092  mbfi1fseqlem6  26096  mbfi1fseq  26097  mbfi1flimlem  26098  mbfmullem  26101  itg2const  26116  itg2mulc  26123  itg2monolem1  26126  itg2i1fseqle  26130  itg2i1fseq  26131  itg2addlem  26134  itg2cnlem1  26137  itg2cn  26139  isibl  26141  isibl2  26142  iblitg  26144  itgeq1  26148  itgz  26156  itgvallem  26160  itgvallem3  26161  iblcnlem1  26163  itgcnlem  26165  iblrelem  26166  iblposlem  26167  iblpos  26168  itgrevallem1  26170  itgposval  26171  iblss2  26181  itgss  26187  itgfsum  26202  iblabslem  26203  iblmulc2  26206  bddmulibl  26214  itgcn  26220  ellimc  26248  dvnfval  26297  cpnfval  26307  dvexp  26328  dvexp2  26329  dvmptfsum  26350  dvlipcn  26369  dvivthlem1  26383  dvfsumle  26396  dvfsumabs  26398  dvfsumlem2  26402  itgpowd  26425  elply2  26569  elplyr  26574  elplyd  26575  coeeu  26599  coelem  26600  coeeq  26601  plyco  26615  coe11  26627  coe1termlem  26632  dgrcolem1  26647  dvply2g  26661  elqaalem3  26701  eltayl  26744  tayl0  26746  taylthlem1  26757  taylthlem2  26758  ulmcau  26779  ulmdvlem1  26784  ulmdvlem3  26786  mtest  26788  mtestbdd  26789  pserval  26794  pserulm  26806  psercn  26810  pserdvlem2  26812  abelthlem3  26817  logtayl  27045  dvcxp1  27125  dvcncxp1  27128  logbmpt  27173  dmarea  27342  lgamgulmlem2  27414  lgamgulmlem5  27417  musum  27575  dchrptlem2  27649  dchrptlem3  27650  dchrpt  27651  lgsval  27685  lgsval4lem  27692  lgsneg  27705  lgsmod  27707  rpvmasum2  27896  padicfval  28000  ostth2  28021  ostth3  28022  ostth  28023  lmif  29347  islmib  29349  incistruhgr  29714  eucrct2eupth  30903  htthlem  31576  htth  31577  pjhfval  32055  hosmval  32394  hommval  32395  hodmval  32396  hfsmval  32397  hfmmval  32398  brafval  32602  kbfval  32611  mptprop  33388  indsn  33526  psgnfzto1st  33765  fxpsubm  33832  fxpsubg  33833  fxpsubrg  33834  elrgspnlem1  33902  elrgspnlem2  33903  elrgspnlem3  33904  elrgspnlem4  33905  elrgspn  33906  elrgspnsubrunlem1  33907  linds2eq  34040  elrspunidl  34082  elrspunsn  34083  evl1deg1  34211  evl1deg2  34212  evl1deg3  34213  evls1rgspncl  34248  mplasclco  34259  selvply1rhmlema  34261  selvply1rhmlemb  34262  selvply1rhmlem2  34264  selvply1rhmlem3  34265  selvply1rhmlem4  34266  selvply1rhmlem5  34267  selvply1rhm  34268  mplidom  34271  extvfval  34275  extvfv  34276  mvrvalind  34281  evlextv  34285  mplvrpmfgalem  34287  mplvrpmga  34288  mplvrpmmhm  34289  mplvrpmrhm  34290  psrgsum  34291  psrmonmul2  34294  psrmonprod  34295  splysubrg  34303  issply  34304  esplyval  34305  esplyfvaln  34317  vietalem  34322  vieta  34323  lbsdiflsp0  34369  fedgmullem1  34372  fedgmullem2  34373  fedgmul  34374  evls1fldgencl  34413  fldextrspunlsplem  34416  fldextrspunlsp  34417  extdgfialglem2  34436  mdetpmtr1  34566  zar0ring  34621  ordtcnvNEW  34663  ordtrest2NEW  34666  xrhval  34761  esum2dlem  34835  ofceq  34840  itgeq12dv  35069  ballotlemfval  35233  vtsval  35377  lpadval  35419  ptpconn  36206  cvmliftlem15  36271  cvmlift2lem4  36279  cvmlift2  36289  snmlval  36304  snmlflim  36305  satf  36326  mrsubfval  36481  mrsubrn  36486  elmsubrn  36501  msubrn  36502  msubco  36504  faclim  36726  faclim2  36728  prodeq12sdv  37222  itgeq12sdv  37223  cbvsumdavw  37283  cbvproddavw  37284  cbvsumdavw2  37299  cbvproddavw2  37300  knoppcnlem1  37574  knoppcnlem6  37579  knoppcnlem7  37580  bj-evaleq  38262  csbrdgg  38520  poimirlem5  38811  poimirlem6  38812  poimirlem7  38813  poimirlem8  38814  poimirlem10  38816  poimirlem11  38817  poimirlem12  38818  poimirlem15  38821  poimirlem16  38822  poimirlem17  38823  poimirlem18  38824  poimirlem19  38825  poimirlem20  38826  poimirlem21  38827  poimirlem22  38828  poimirlem27  38833  voliunnfl  38850  itg2addnclem  38857  itg2addnclem3  38859  itg2addnc  38860  itg2gt0cn  38861  iblabsnclem  38869  iblmulc2nc  38871  ftc1anclem2  38880  ftc1anclem6  38884  ftc1anclem8  38886  ftc1anc  38887  ftc2nc  38888  upixp  38931  rrncmslem  39032  ismrer1  39038  tendoplcbv  42098  tendopl  42099  tendoicbv  42116  tendoi  42117  dihfval  42554  lcfl7N  42824  lcfrlem8  42872  lcfrlem9  42873  lcf1o  42874  hvmapval  43083  hdmap1fval  43119  hdmapffval  43149  hdmapfval  43150  hgmapffval  43208  hgmapfval  43209  lcmineqlem7  43351  lcmineqlem12  43356  aks6d1c6lem5  43493  rhmpsr  43877  evlsbagval  43880  evlselv  43883  fsuppind  43884  fsuppssindlem2  43886  fsuppssind  43887  mzpclval  44002  mzpcl2  44007  mzpexpmpt  44022  mzpsubst  44025  mzpcompact2lem  44028  rmxfval  44177  rmyfval  44178  aomclem8  44329  hbtlem1  44390  hbtlem7  44392  rfovfvd  45263  fsovrfovd  45270  fsovfvd  45271  fsovcnvlem  45274  dssmapfv2d  45279  dssmapnvod  45281  ntrneibex  45334  mnringmulrvald  45486  mnringmulrcld  45487  expgrowthi  45578  expgrowth  45580  binomcxplemdvsum  45600  addrval  45708  subrval  45709  mulvval  45710  fmulcl  46866  fmuldfeqlem1  46867  fprodcnlem  46884  fprodcn  46885  fnlimfv  46946  fnlimcnv  46950  fnlimfvre  46957  fnlimfvre2  46960  fnlimf  46961  fnlimabslt  46962  liminfval  47042  limsupresxr  47049  liminfresxr  47050  liminfvalxr  47066  fprodcncf  47183  dvnmptdivc  47221  dvnxpaek  47225  dvnmul  47226  dvmptfprod  47228  dvnprodlem1  47229  dvnprodlem2  47230  dvnprodlem3  47231  dvnprod  47232  stoweidlem2  47285  stoweidlem17  47300  stoweidlem19  47302  stoweidlem20  47303  stoweidlem43  47326  stoweidlem62  47345  stoweid  47346  dirkercncflem2  47387  fourierdlem112  47501  fourierdlem113  47502  etransclem1  47518  etransclem5  47522  etransclem17  47534  etransclem19  47536  etransclem22  47539  sge0val  47649  ovnlecvr  47841  ovncvrrp  47847  ovn0lem  47848  ovnsubaddlem1  47853  ovnsubadd  47855  hsphoif  47859  hsphoival  47862  hoidmv1lelem1  47874  hoidmv1lelem2  47875  hoidmv1lelem3  47876  hoidmv1le  47877  hoidmvlelem1  47878  hoidmvlelem2  47879  hoidmvlelem3  47880  hoidmvlelem4  47881  hoidmvlelem5  47882  hoidmvle  47883  ovnhoilem1  47884  ovnhoi  47886  hoidifhspval  47891  ovncvr2  47894  hoidifhspval2  47898  hspmbllem2  47910  hspmbllem3  47911  hspmbl  47912  ovnovollem1  47939  vonioolem2  47964  vonioo  47965  vonicclem2  47967  vonicc  47968  smflimlem4  48057  smflim  48060  smflim2  48089  smfsuplem2  48095  smfsup  48097  smfinf  48101  smflimsuplem2  48104  smflimsuplem5  48107  smflimsuplem7  48109  smflimsup  48111  cfsetsnfsetfo  48403  linply  49713  lincop  49851  1arymaptfv  50083  itcoval  50104  itcovalpc  50115  itcovalt2  50120  ackvalsuc1mpt  50121  ackval1  50124  fuco21  50789  postcof2  50831  prcofval  50844  aacllem  51367  crosspval  51382  crosspdot0lem  51391  veronesevald  51399  veronesematrowexpd  51410