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

Theorem feq1d 5572
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 5568 . 2  |-  ( F  =  G  ->  ( F : A --> B  <->  G : A
--> B ) )
31, 2syl 16 1  |-  ( ph  ->  ( F : A --> B 
<->  G : A --> B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1652   -->wf 5442
This theorem is referenced by:  feq12d  5574  fco2  5593  fssres2  5603  fresin  5604  fresaun  5606  fmptco  5893  fressnfv  5912  off  6312  caofinvl  6323  curry1f  6432  curry2f  6434  f2ndf  6444  eroprf  6994  pmresg  7033  pw2f1olem  7204  ordtypelem4  7482  fseqenlem1  7897  canthp1lem2  8520  fseq1p1m1  11114  s1cl  11747  rlimres  12344  lo1res  12345  rpnnen2lem2  12807  1arithlem3  13285  vdwapf  13332  mrcf  13826  cofucl  14077  funcres  14085  homaf  14177  1stfcl  14286  2ndfcl  14287  prfcl  14292  evlfcl  14311  curf1cl  14317  yonedalem4c  14366  vrmdf  14795  pj1f  15321  efgtf  15346  vrgpf  15392  gsumzres  15509  lspf  16042  psrass1lem  16434  subrgpsr  16474  mvrf  16480  coe1f2  16599  isphld  16877  pjf  16932  lmbr  17314  tsmsres  18165  prdsdsf  18389  imasdsf1olem  18395  blfps  18428  blf  18429  nmf2  18632  tngngp2  18685  nmof  18745  cphnmf  19150  ovolctb  19378  uniioombllem2  19467  mbfi1fseqlem3  19601  itg2monolem1  19634  itg2monolem2  19635  itg2monolem3  19636  itg2mono  19637  itg2cnlem1  19645  dvres  19790  dvres3a  19793  dvnff  19801  dvcmulf  19823  dvmptcl  19837  dvmptco  19850  dvlipcn  19870  dvgt0lem1  19878  dvle  19883  itgsubstlem  19924  dgrlem  20140  taylpf  20274  taylthlem1  20281  ulmval  20288  ulmshftlem  20297  ulmshft  20298  ulmdvlem1  20308  psergf  20320  pserdvlem2  20336  lgsfcl3  21093  vdgrf  21661  vdgrfif  21662  grpodivf  21826  nvmf  22119  imsdf  22173  ipf  22204  0oo  22282  hoaddcl  23253  homulcl  23254  hosubcl  23268  brafn  23442  kbop  23448  off2  24046  fmpt3d  24062  fmptcof2  24068  ofoprabco  24071  indf1ofs  24415  cvmliftlem6  24969  cvmliftlem10  24973  ftc1anclem3  26272  tailf  26395  rrnmet  26529  pw2f1ocnv  27099  uvcff  27208  frlmup1  27218  pmtrf  27365  pmtrfinv  27370  pmtrff1o  27372  pmtrfcnv  27373  psgnunilem5  27385  seff  27506  expgrowth  27520  stoweidlem34  27750  stoweidlem42  27758  stoweidlem48  27764  tendoplcl  31515  tendoicl  31530
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-rab 2706  df-v 2950  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-br 4205  df-opab 4259  df-rel 4877  df-cnv 4878  df-co 4879  df-dm 4880  df-rn 4881  df-fun 5448  df-fn 5449  df-f 5450
  Copyright terms: Public domain W3C validator