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

Theorem feq1d 5534
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 5530 . 2  |-  ( F  =  G  ->  ( F : A --> B  <->  G : A
--> B ) )
31, 2syl 16 1  |-  ( ph  ->  ( F : A --> B 
<->  G : A --> B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1362   -->wf 5402
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-br 4281  df-opab 4339  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-fun 5408  df-fn 5409  df-f 5410
This theorem is referenced by:  feq12d  5536  fco2  5557  fssres2  5567  fresin  5568  fresaun  5570  fmptco  5863  fressnfv  5883  off  6323  caofinvl  6336  curry1f  6655  curry2f  6657  f2ndf  6667  eroprf  7186  pmresg  7228  pw2f1olem  7403  ordtypelem4  7723  fseqenlem1  8182  canthp1lem2  8808  fseq1p1m1  11518  repsf  12395  rlimres  13020  lo1res  13021  rpnnen2lem2  13481  1arithlem3  13969  vdwapf  14016  fsets  14183  mrcf  14530  cofucl  14781  funcres  14789  homaf  14881  1stfcl  14990  2ndfcl  14991  prfcl  14996  evlfcl  15015  curf1cl  15021  yonedalem4c  15070  vrmdf  15516  pmtrf  15941  pmtrfinv  15947  pmtrff1o  15949  pmtrfcnv  15950  psgnunilem5  15980  pj1f  16174  efgtf  16199  vrgpf  16245  gsumzres  16368  gsumzresOLD  16372  gsummptfsadd  16394  gsummptfsaddOLD  16395  lspf  16977  psrass1lem  17381  subrgpsr  17425  mvrf  17431  coe1f2  17564  isphld  17925  pjf  17980  uvcff  18058  frlmup1  18068  lmbr  18704  tsmsresOLD  19559  tsmsres  19560  prdsdsf  19784  imasdsf1olem  19790  blfps  19823  blf  19824  nmf2  20027  tngngp2  20080  nmof  20140  cphnmf  20556  rrxmet  20749  ovolctb  20815  uniioombllem2  20905  mbfi1fseqlem3  21037  itg2monolem1  21070  itg2monolem2  21071  itg2monolem3  21072  itg2mono  21073  itg2cnlem1  21081  dvres  21228  dvres3a  21231  dvnff  21239  dvcmulf  21261  dvmptcl  21275  dvmptco  21288  dvlipcn  21308  dvgt0lem1  21316  dvle  21321  itgsubstlem  21362  dgrlem  21582  taylpf  21716  taylthlem1  21723  ulmval  21730  ulmshftlem  21739  ulmshft  21740  ulmdvlem1  21750  psergf  21762  pserdvlem2  21778  lgsfcl3  22541  vdgrf  23391  vdgrfif  23392  grpodivf  23556  nvmf  23849  imsdf  23903  ipf  23934  0oo  24012  hoaddcl  24985  homulcl  24986  hosubcl  25000  brafn  25174  kbop  25180  off2  25783  fmpt3d  25797  fmptcof2  25803  ofoprabco  25806  fpwrelmap  25858  indf1ofs  26336  fibp1  26632  ccatmulgnn0dir  26788  signstf  26815  cvmliftlem6  27027  cvmliftlem10  27031  ftc1anclem3  28313  tailf  28440  rrnmet  28572  pw2f1ocnv  29231  itgpowd  29435  seff  29440  expgrowth  29454  stoweidlem34  29675  stoweidlem42  29683  stoweidlem48  29689  tendoplcl  34019  tendoicl  34034
  Copyright terms: Public domain W3C validator