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

Theorem feq1d 5395
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 5391 . 2  |-  ( F  =  G  ->  ( F : A --> B  <->  G : A
--> B ) )
31, 2syl 15 1  |-  ( ph  ->  ( F : A --> B 
<->  G : A --> B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1632   -->wf 5267
This theorem is referenced by:  feq12d  5397  fco2  5415  fssres2  5425  fresin  5426  fresaun  5428  fmptco  5707  fressnfv  5723  off  6109  caofinvl  6120  curry1f  6228  curry2f  6230  eroprf  6772  pmresg  6811  pw2f1olem  6982  ordtypelem4  7252  fseqenlem1  7667  canthp1lem2  8291  fseq1p1m1  10873  s1cl  11457  rlimres  12048  lo1res  12049  rpnnen2lem2  12510  1arithlem3  12988  vdwapf  13035  mrcf  13527  cofucl  13778  funcres  13786  homaf  13878  1stfcl  13987  2ndfcl  13988  prfcl  13993  evlfcl  14012  curf1cl  14018  yonedalem4c  14067  vrmdf  14496  pj1f  15022  efgtf  15047  vrgpf  15093  gsumzres  15210  lspf  15747  psrass1lem  16139  subrgpsr  16179  mvrf  16185  coe1f2  16306  isphld  16574  pjf  16629  lmbr  17004  tsmsres  17842  prdsdsf  17947  imasdsf1olem  17953  blf  17977  nmf2  18131  tngngp2  18184  nmof  18244  cphnmf  18647  iscau  18718  ovolctb  18865  uniioombllem2  18954  mbfi1fseqlem3  19088  itg2monolem1  19121  itg2monolem2  19122  itg2monolem3  19123  itg2mono  19124  itg2cnlem1  19132  dvres  19277  dvres3a  19280  dvnff  19288  dvcmulf  19310  dvmptcl  19324  dvmptco  19337  dvlipcn  19357  dvgt0lem1  19365  dvle  19370  itgsubstlem  19411  dgrlem  19627  taylpf  19761  taylthlem1  19768  ulmval  19775  ulmshftlem  19784  ulmshft  19785  ulmdvlem1  19793  psergf  19804  pserdvlem2  19820  lgsfcl3  20572  grpodivf  20929  isrngo  21061  nvmf  21220  imsdf  21274  ipf  21305  0oo  21383  hoaddcl  22354  homulcl  22355  hosubcl  22369  brafn  22543  kbop  22549  off2  23223  fmpt3d  23237  fmptcof2  23244  ofoprabco  23247  ofcf  23479  mbfmcst  23579  indf1ofs  23624  cvmliftlem6  23836  cvmliftlem10  23840  vdgrf  23906  prmapcp2  25260  prjmapcp  25268  sigadd  25752  fnmulcv  25787  domcatfun  26028  codcatfun  26037  idcatfun  26044  tailf  26427  rrnmet  26656  pw2f1ocnv  27233  uvcff  27343  frlmup1  27353  pmtrf  27500  pmtrfinv  27505  pmtrff1o  27507  pmtrfcnv  27508  psgnunilem5  27520  seff  27641  expgrowth  27655  stoweidlem34  27886  stoweidlem42  27894  stoweidlem48  27900  tendoplcl  31592  tendoicl  31607
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-br 4040  df-opab 4094  df-rel 4712  df-cnv 4713  df-co 4714  df-dm 4715  df-rn 4716  df-fun 5273  df-fn 5274  df-f 5275
  Copyright terms: Public domain W3C validator