Theorem mpteq2dv 4673

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

Syntax hints:   → wi 4   = wceq 1475   ∈ wcel 1977   ↦ cmpt 4643

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-ral 2901  df-opab 4644  df-mpt 4645

This theorem is referenced by:  ofeq  6797  mpt2curryvald  7283  rdgeq1  7394  rdgeq2  7395  omv  7479  oev  7481  oieq1  8300  oieq2  8301  cantnflem1  8469  wunex2  9439  wuncval2  9448  rpnnen1  11696  seqof2  12721  relexpsucnnr  13613  relexp1g  13614  limsupval  14053  sumeq2w  14270  sumeq2ii  14271  cbvsum  14273  summo  14295  fsum  14298  fsumrlim  14384  fsumo1  14385  prodeq2w  14481  prodmo  14505  fprod  14510  bpolylem  14618  rpnnen2lem1  14782  rpnnen2lem2  14783  1arithlem1  15465  vdwapval  15515  vdwlem6  15528  vdwlem8  15530  vdwlem9  15531  vdwlem10  15532  ramub1lem2  15569  ramcl  15571  prdsplusgval  15956  prdsmulrval  15958  prdsdsval  15961  prdsvscaval  15962  ismon  16216  fucco  16445  curf1  16688  curf2  16692  yonedalem4a  16738  grplactfval  17339  galactghm  17646  pmtrval  17694  sylow1  17841  sylow2b  17861  sylow3lem5  17869  sylow3  17871  iscyg  18104  gsumzaddlem  18144  gsumzmhm  18160  ablfac2  18311  gsumdixp  18432  fczpsrbag  19188  psrmulfval  19206  mvrval  19242  subrgmvr  19282  mplcoe1  19286  mplcoe3  19287  mplcoe5  19289  mplmon2  19314  subrgascl  19319  evlslem2  19333  evlslem3  19335  evlslem1  19336  mpfrcl  19339  evlsval  19340  evlsvar  19344  mpfind  19357  coe1fval  19396  pf1ind  19540  evl1gsumadd  19543  zncyg  19716  phllmhm  19796  isphld  19818  frlmgsum  19930  frlmipval  19937  frlmphl  19939  uvcval  19943  mamuval  20011  mamufv  20012  matgsum  20062  madetsumid  20086  mat1dimmul  20101  mvmulval  20168  mvmulfv  20169  mavmulfv  20171  1mavmul  20173  marepvval0  20191  mulmarep1gsum1  20198  mdetleib  20212  mdetleib2  20213  mdetfval1  20215  mdetleib1  20216  mdet0pr  20217  m1detdiag  20222  mdetralt  20233  mdetunilem9  20245  m2detleib  20256  smadiadetlem3  20293  mat2pmatmul  20355  decpmatmul  20396  decpmatmulsumfsupp  20397  pmatcollpw1  20400  monmatcollpw  20403  pmatcollpw3lem  20407  pmatcollpw3fi1lem2  20411  pm2mpval  20419  pm2mpfval  20420  mply1topmatval  20428  mp2pm2mplem1  20430  mp2pm2mplem3  20432  ptbasfi  21194  ptcnplem  21234  ptrescn  21252  cnmpt2k  21301  xkohmeo  21428  fmval  21557  fmf  21559  ptcmpg  21671  tmdmulg  21706  prdstmdd  21737  tsmspropd  21745  prdsxmslem2  22144  metdsval  22458  fsumcn  22481  expcn  22483  lebnumlem3  22570  pcoval  22619  pi1xfrcnv  22665  rrxds  22989  rrxmval  22996  itg11  23264  mbfi1fseqlem2  23289  mbfi1fseqlem6  23293  mbfi1fseq  23294  mbfi1flimlem  23295  mbfmullem  23298  itg2const  23313  itg2mulc  23320  itg2monolem1  23323  itg2i1fseqle  23327  itg2i1fseq  23328  itg2addlem  23331  itg2cnlem1  23334  itg2cn  23336  isibl  23338  isibl2  23339  iblitg  23341  itgz  23353  itgvallem  23357  itgvallem3  23358  iblcnlem1  23360  itgcnlem  23362  iblrelem  23363  iblposlem  23364  iblpos  23365  itgrevallem1  23367  itgposval  23368  iblss2  23378  itgss  23384  itgfsum  23399  iblabslem  23400  iblmulc2  23403  bddmulibl  23411  itgcn  23415  ellimc  23443  dvnfval  23491  cpnfval  23501  dvexp  23522  dvexp2  23523  dvmptfsum  23542  dvlipcn  23561  dvivthlem1  23575  dvfsumle  23588  dvfsumabs  23590  dvfsumlem2  23594  elply2  23756  elplyr  23761  elplyd  23762  coeeu  23785  coelem  23786  coeeq  23787  plyco  23801  coe11  23813  coe1termlem  23818  dgrcolem1  23833  dvply2g  23844  elqaalem3  23880  eltayl  23918  tayl0  23920  taylthlem1  23931  taylthlem2  23932  ulmcau  23953  ulmdvlem1  23958  ulmdvlem3  23960  mtest  23962  mtestbdd  23963  pserval  23968  pserulm  23980  psercn  23984  pserdvlem2  23986  abelthlem3  23991  logtayl  24206  dvcxp1  24281  dvcncxp1  24284  logbmpt  24326  dmarea  24484  lgamgulmlem2  24556  lgamgulmlem5  24559  musum  24717  dchrptlem2  24790  dchrptlem3  24791  dchrpt  24792  lgsval  24826  lgsval4lem  24833  lgsneg  24846  lgsmod  24848  rpvmasum2  25001  padicfval  25105  ostth2  25126  ostth3  25127  ostth  25128  lmif  25477  islmib  25479  incistruhgr  25746  wwlkn  26210  clwwlkn  26295  clwwlknprop  26300  htthlem  27158  htth  27159  pjhfval  27639  hosmval  27978  hommval  27979  hodmval  27980  hfsmval  27981  hfmmval  27982  brafval  28186  kbfval  28195  psgnfzto1st  29186  mdetpmtr1  29217  ordtcnvNEW  29294  ordtrest2NEW  29297  xrhval  29390  indval  29403  esum2dlem  29481  ofceq  29486  itgeq12dv  29715  ballotlemfval  29878  ptpcon  30469  cvmliftlem15  30534  cvmlift2lem4  30542  cvmlift2  30552  snmlval  30567  snmlflim  30568  mrsubfval  30659  mrsubrn  30664  elmsubrn  30679  msubrn  30680  msubco  30682  faclim  30885  faclim2  30887  trpredeq1  30964  trpredeq2  30965  knoppcnlem1  31653  knoppcnlem6  31658  knoppcnlem7  31659  csbrdgg  32351  curfv  32559  matunitlindflem2  32576  poimirlem5  32584  poimirlem6  32585  poimirlem7  32586  poimirlem8  32587  poimirlem10  32589  poimirlem11  32590  poimirlem12  32591  poimirlem15  32594  poimirlem16  32595  poimirlem17  32596  poimirlem18  32597  poimirlem19  32598  poimirlem20  32599  poimirlem21  32600  poimirlem22  32601  poimirlem27  32606  voliunnfl  32623  itg2addnclem  32631  itg2addnclem3  32633  itg2addnc  32634  itg2gt0cn  32635  iblabsnclem  32643  iblmulc2nc  32645  ftc1anclem2  32656  ftc1anclem6  32660  ftc1anclem8  32662  ftc1anc  32663  ftc2nc  32664  upixp  32694  rrncmslem  32801  ismrer1  32807  tendoplcbv  35081  tendopl  35082  tendoicbv  35099  tendoi  35100  dihfval  35538  lcfl7N  35808  lcfrlem8  35856  lcfrlem9  35857  lcf1o  35858  hvmapval  36067  hdmap1fval  36104  hdmapffval  36136  hdmapfval  36137  hgmapffval  36195  hgmapfval  36196  mzpclval  36306  mzpcl2  36311  mzpexpmpt  36326  mzpsubst  36329  mzpcompact2lem  36332  rmxfval  36486  rmyfval  36487  aomclem8  36649  hbtlem1  36712  hbtlem7  36714  itgpowd  36819  rfovfvd  37316  fsovrfovd  37323  fsovfvd  37324  fsovcnvlem  37327  dssmapfv2d  37332  dssmapnvod  37334  ntrneibex  37391  expgrowthi  37554  expgrowth  37556  binomcxplemdvsum  37576  addrval  37691  subrval  37692  mulvval  37693  fmulcl  38648  fmuldfeqlem1  38649  fprodcnlem  38666  fprodcn  38667  fnlimfv  38730  fnlimcnv  38734  fnlimfvre  38741  fnlimfvre2  38744  fnlimf  38745  fnlimabslt  38746  fprodcncf  38787  dvnmptdivc  38828  dvnxpaek  38832  dvnmul  38833  dvmptfprod  38835  dvnprodlem1  38836  dvnprodlem2  38837  dvnprodlem3  38838  dvnprod  38839  stoweidlem2  38895  stoweidlem17  38910  stoweidlem19  38912  stoweidlem20  38913  stoweidlem43  38936  stoweidlem62  38955  stoweid  38956  dirkercncflem2  38997  fourierdlem112  39111  fourierdlem113  39112  etransclem1  39128  etransclem5  39132  etransclem17  39144  etransclem19  39146  etransclem22  39149  sge0val  39259  ovnlecvr  39448  ovncvrrp  39454  ovn0lem  39455  ovnsubaddlem1  39460  ovnsubadd  39462  hsphoif  39466  hsphoival  39469  hoidmv1lelem1  39481  hoidmv1lelem2  39482  hoidmv1lelem3  39483  hoidmv1le  39484  hoidmvlelem1  39485  hoidmvlelem2  39486  hoidmvlelem3  39487  hoidmvlelem4  39488  hoidmvlelem5  39489  hoidmvle  39490  ovnhoilem1  39491  ovnhoi  39493  hoidifhspval  39498  ovncvr2  39501  hoidifhspval2  39505  hspmbllem2  39517  hspmbllem3  39518  hspmbl  39519  ovnovollem1  39546  vonioolem2  39572  vonioo  39573  vonicclem2  39575  vonicc  39576  smflimlem4  39660  smflim  39663  eucrct2eupth  41413  c0rhm  41702  c0rnghm  41703  lincop  41991  aacllem  42356