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

Theorem feq1d 5732
Description: Equality deduction for functions. (Contributed by NM, 19-Feb-2008.)
Hypothesis
Ref Expression
feq1d.1  |-  ( ph  ->  F  =  G )
Assertion
Ref Expression
feq1d  |-  ( ph  ->  ( F : A --> B 
<->  G : A --> B ) )

Proof of Theorem feq1d
StepHypRef Expression
1 feq1d.1 . 2  |-  ( ph  ->  F  =  G )
2 feq1 5728 . 2  |-  ( F  =  G  ->  ( F : A --> B  <->  G : A
--> B ) )
31, 2syl 17 1  |-  ( ph  ->  ( F : A --> B 
<->  G : A --> B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    = wceq 1437   -->wf 5597
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-rab 2791  df-v 3089  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-sn 4003  df-pr 4005  df-op 4009  df-br 4427  df-opab 4485  df-rel 4861  df-cnv 4862  df-co 4863  df-dm 4864  df-rn 4865  df-fun 5603  df-fn 5604  df-f 5605
This theorem is referenced by:  feq12d  5735  fco2  5757  fssres2  5768  fresin  5769  fresaun  5771  fmpt3d  6062  fmptco  6071  fressnfv  6093  off  6560  caofinvl  6572  curry1f  6901  curry2f  6903  f2ndf  6913  eroprf  7469  pmresg  7507  pw2f1olem  7682  ordtypelem4  8036  fseqenlem1  8453  canthp1lem2  9077  fseq1p1m1  11866  repsf  12861  rlimres  13600  lo1res  13601  rpnnen2lem2  14246  1arithlem3  14832  vdwapf  14885  fsets  15112  mrcf  15466  cofucl  15744  funcres  15752  homaf  15876  funcestrcsetclem3  15978  funcestrcsetclem9  15984  funcsetcestrclem3  15992  1stfcl  16033  2ndfcl  16034  prfcl  16039  evlfcl  16058  curf1cl  16064  yonedalem4c  16113  vrmdf  16593  pmtrf  17047  pmtrfinv  17053  pmtrff1o  17055  pmtrfcnv  17056  psgnunilem5  17086  pj1f  17282  efgtf  17307  vrgpf  17353  gsumzres  17478  gsummptfsadd  17492  gsummptfssub  17517  lspf  18132  psrass1lem  18536  subrgpsr  18578  mvrf  18583  coe1f2  18737  isphld  19152  pjf  19207  uvcff  19280  frlmup1  19287  cpm2mf  19707  lmbr  20205  tsmsres  21089  prdsdsf  21313  imasdsf1olem  21319  blfps  21352  blf  21353  nmf2  21538  tngngp2  21591  nmof  21651  cphnmf  22066  rrxmet  22255  ovolctb  22321  uniioombllem2  22417  uniioombllem2OLD  22418  mbfi1fseqlem3  22552  itg2monolem1  22585  itg2monolem2  22586  itg2monolem3  22587  itg2mono  22588  itg2cnlem1  22596  dvres  22743  dvres3a  22746  dvnff  22754  dvcmulf  22776  dvmptcl  22790  dvmptco  22803  dvlipcn  22823  dvgt0lem1  22831  dvle  22836  itgsubstlem  22877  dgrlem  23051  taylpf  23186  taylthlem1  23193  ulmval  23200  ulmshftlem  23209  ulmshft  23210  ulmdvlem1  23220  psergf  23232  pserdvlem2  23248  logbf  23591  lgsfcl3  24108  midf  24674  lmif  24683  vdgrf  25471  vdgrfif  25472  grpodivf  25819  nvmf  26112  imsdf  26166  ipf  26197  0oo  26275  hoaddcl  27246  homulcl  27247  hosubcl  27261  brafn  27435  kbop  27441  off2  28082  fmptcof2  28099  ofoprabco  28107  fpwrelmap  28161  indf1ofs  28686  fibp1  29060  ccatmulgnn0dir  29216  cvmliftlem6  29801  cvmliftlem10  29805  mrsubff  29938  msubff  29956  tailf  30816  poimirlem24  31668  ftc1anclem3  31723  rrnmet  31865  tendoplcl  34057  tendoicl  34072  pw2f1ocnv  35598  itgpowd  35798  seff  36294  expgrowth  36321  feq1dd  37052  dvnmul  37387  dvnprodlem2  37391  dvnprodlem3  37392  stoweidlem34  37464  stoweidlem42  37472  stoweidlem48  37478  dirkerf  37528  fourierdlem41  37579  fourierdlem51  37589  fourierdlem57  37595  fourierdlem60  37598  fourierdlem61  37599  fourierdlem73  37611  fourierdlem75  37613  fourierdlem103  37641  fourierdlem104  37642  etransclem1  37667  etransclem2  37668  etransclem20  37686  etransclem33  37699  etransclem46  37712  pfxf  38320  funcringcsetcALTV2lem3  38798  funcringcsetcALTV2lem9  38804  funcringcsetclem3ALTV  38821  funcringcsetclem9ALTV  38827  fdivmptf  39113  refdivmptf  39114
  Copyright terms: Public domain W3C validator