MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  feq1d Structured version   Visualization version   GIF version

Theorem feq1d 6658
Description: Equality deduction for functions. (Contributed by NM, 19-Feb-2008.)
Hypothesis
Ref Expression
feq1d.1 (𝜑𝐹 = 𝐺)
Assertion
Ref Expression
feq1d (𝜑 → (𝐹:𝐴𝐵𝐺:𝐴𝐵))

Proof of Theorem feq1d
StepHypRef Expression
1 feq1d.1 . 2 (𝜑𝐹 = 𝐺)
2 feq1 6654 . 2 (𝐹 = 𝐺 → (𝐹:𝐴𝐵𝐺:𝐴𝐵))
31, 2syl 17 1 (𝜑 → (𝐹:𝐴𝐵𝐺:𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1542  wf 6497
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3411  df-v 3450  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-br 5111  df-opab 5173  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-fun 6503  df-fn 6504  df-f 6505
This theorem is referenced by:  feq12d  6661  fco2  6700  fssres2  6715  fresin  6716  fresaun  6718  fmpt3d  7069  fressnfv  7111  f2ndf  8057  eroprf  8761  pmresg  8815  pw2f1olem  9027  ordtypelem4  9464  canthp1lem2  10596  fseq1p1m1  13522  repsf  14668  rlimres  15447  lo1res  15448  vdwapf  16851  fsets  17048  mrcf  17496  cofucl  17781  funcres  17789  funcestrcsetclem9  18043  1stfcl  18092  2ndfcl  18093  evlfcl  18118  yonedalem4c  18173  pmtrfinv  19250  pmtrff1o  19252  pmtrfcnv  19253  efgtf  19511  gsumzres  19693  isphld  21074  pjf  21135  frlmup1  21220  psrass1lemOLD  21358  psrass1lem  21361  coe1f2  21596  lmbr  22625  tsmsres  23511  prdsdsf  23736  imasdsf1olem  23742  blfps  23775  blf  23776  tngngp2  24032  rrxmet  24788  ovolctb  24870  itg2monolem1  25131  itg2monolem2  25132  itg2monolem3  25133  itg2mono  25134  dvres  25291  dvres3a  25294  dvnff  25303  dvcmulf  25325  dvmptcl  25339  dvmptco  25352  dvlipcn  25374  dvgt0lem1  25382  itgsubstlem  25428  itgpowd  25430  dgrlem  25606  taylthlem1  25748  ulmval  25755  lgsfcl3  26682  midf  27760  grpodivf  29522  nvmf  29629  imsdf  29673  ipf  29697  0oo  29773  hoaddcl  30742  homulcl  30743  hosubcl  30757  fmptcof2  31615  ofoprabco  31622  fpwrelmap  31692  fedgmullem1  32364  indf1ofs  32665  sitmf  32992  fibp1  33041  ccatmulgnn0dir  33194  reprsuc  33268  pfxwlk  33757  cvmliftlem6  33924  cvmliftlem10  33928  mrsubff  34146  msubff  34164  tailf  34876  curf  36085  uncf  36086  poimirlem24  36131  ftc1anclem3  36182  rrnmet  36317  tendoplcl  39273  tendoicl  39288  intlewftc  40547  pw2f1ocnv  41390  seff  42663  expgrowth  42689  feq1dd  43458  dvnmul  44258  dvnprodlem2  44262  dvnprodlem3  44263  voliooicof  44311  stoweidlem34  44349  stoweidlem42  44357  stoweidlem48  44363  dirkerf  44412  fourierdlem41  44463  fourierdlem51  44472  fourierdlem57  44478  fourierdlem60  44481  fourierdlem61  44482  fourierdlem73  44494  fourierdlem75  44496  fourierdlem103  44524  fourierdlem104  44525  etransclem1  44550  etransclem2  44551  etransclem20  44569  etransclem33  44582  etransclem46  44595  sge0isum  44742  sge0seq  44761  isomenndlem  44845  hoicvr  44863  ovnf  44878  ovnsubaddlem1  44885  hsphoif  44891  hoidmvlelem2  44911  hoidmvlelem3  44912  ovnhoilem1  44916  ovnhoilem2  44917  ovncvr2  44926  hoidifhspf  44933  hspmbllem2  44942  iccvonmbllem  44993  vonioolem1  44995  vonioolem2  44996  vonicclem1  44998  vonicclem2  44999  smfsupdmmbllem  45159  smfinfdmmbllem  45163  fsetsniunop  45357  1hegrlfgr  46108  funcringcsetcALTV2lem3  46410  funcringcsetcALTV2lem9  46416  funcringcsetclem3ALTV  46433  funcringcsetclem9ALTV  46439  fdivmptf  46701  refdivmptf  46702  itcovalendof  46829  ackendofnn0  46844
  Copyright terms: Public domain W3C validator