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

Theorem feq1d 5653
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 5649 . 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 1370   -->wf 5521
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rab 2807  df-v 3078  df-dif 3438  df-un 3440  df-in 3442  df-ss 3449  df-nul 3745  df-if 3899  df-sn 3985  df-pr 3987  df-op 3991  df-br 4400  df-opab 4458  df-rel 4954  df-cnv 4955  df-co 4956  df-dm 4957  df-rn 4958  df-fun 5527  df-fn 5528  df-f 5529
This theorem is referenced by:  feq12d  5655  fco2  5676  fssres2  5686  fresin  5687  fresaun  5689  fmptco  5984  fressnfv  6004  off  6443  caofinvl  6456  curry1f  6775  curry2f  6777  f2ndf  6787  eroprf  7307  pmresg  7349  pw2f1olem  7524  ordtypelem4  7845  fseqenlem1  8304  canthp1lem2  8930  fseq1p1m1  11650  repsf  12528  rlimres  13153  lo1res  13154  rpnnen2lem2  13615  1arithlem3  14103  vdwapf  14150  fsets  14317  mrcf  14665  cofucl  14916  funcres  14924  homaf  15016  1stfcl  15125  2ndfcl  15126  prfcl  15131  evlfcl  15150  curf1cl  15156  yonedalem4c  15205  vrmdf  15654  pmtrf  16079  pmtrfinv  16085  pmtrff1o  16087  pmtrfcnv  16088  psgnunilem5  16118  pj1f  16314  efgtf  16339  vrgpf  16385  gsumzres  16508  gsumzresOLD  16512  gsummptfsadd  16534  gsummptfsaddOLD  16535  lspf  17177  psrass1lem  17569  subrgpsr  17614  mvrf  17620  coe1f2  17788  isphld  18207  pjf  18262  uvcff  18340  frlmup1  18350  lmbr  18993  tsmsresOLD  19848  tsmsres  19849  prdsdsf  20073  imasdsf1olem  20079  blfps  20112  blf  20113  nmf2  20316  tngngp2  20369  nmof  20429  cphnmf  20845  rrxmet  21038  ovolctb  21104  uniioombllem2  21195  mbfi1fseqlem3  21327  itg2monolem1  21360  itg2monolem2  21361  itg2monolem3  21362  itg2mono  21363  itg2cnlem1  21371  dvres  21518  dvres3a  21521  dvnff  21529  dvcmulf  21551  dvmptcl  21565  dvmptco  21578  dvlipcn  21598  dvgt0lem1  21606  dvle  21611  itgsubstlem  21652  dgrlem  21829  taylpf  21963  taylthlem1  21970  ulmval  21977  ulmshftlem  21986  ulmshft  21987  ulmdvlem1  21997  psergf  22009  pserdvlem2  22025  lgsfcl3  22788  vdgrf  23719  vdgrfif  23720  grpodivf  23884  nvmf  24177  imsdf  24231  ipf  24262  0oo  24340  hoaddcl  25313  homulcl  25314  hosubcl  25328  brafn  25502  kbop  25508  off2  26109  fmpt3d  26123  fmptcof2  26129  ofoprabco  26132  fpwrelmap  26183  indf1ofs  26626  fibp1  26927  ccatmulgnn0dir  27083  signstf  27110  cvmliftlem6  27322  cvmliftlem10  27326  ftc1anclem3  28616  tailf  28743  rrnmet  28875  pw2f1ocnv  29533  itgpowd  29737  seff  29742  expgrowth  29756  stoweidlem34  29976  stoweidlem42  29984  stoweidlem48  29990  gsummptfssub  30952  tendoplcl  34748  tendoicl  34763
  Copyright terms: Public domain W3C validator