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

Theorem feq1d 5715
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 5711 . 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 1379   -->wf 5582
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-br 4448  df-opab 4506  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-fun 5588  df-fn 5589  df-f 5590
This theorem is referenced by:  feq12d  5718  fco2  5740  fssres2  5751  fresin  5752  fresaun  5754  fmptco  6052  fressnfv  6073  off  6536  caofinvl  6549  curry1f  6874  curry2f  6876  f2ndf  6886  eroprf  7406  pmresg  7443  pw2f1olem  7618  ordtypelem4  7942  fseqenlem1  8401  canthp1lem2  9027  fseq1p1m1  11748  repsf  12704  rlimres  13340  lo1res  13341  rpnnen2lem2  13806  1arithlem3  14298  vdwapf  14345  fsets  14512  mrcf  14860  cofucl  15111  funcres  15119  homaf  15211  1stfcl  15320  2ndfcl  15321  prfcl  15326  evlfcl  15345  curf1cl  15351  yonedalem4c  15400  vrmdf  15849  pmtrf  16276  pmtrfinv  16282  pmtrff1o  16284  pmtrfcnv  16285  psgnunilem5  16315  pj1f  16511  efgtf  16536  vrgpf  16582  gsumzres  16705  gsumzresOLD  16709  gsummptfsadd  16731  gsummptfsaddOLD  16732  gsummptfssub  16767  lspf  17403  psrass1lem  17800  subrgpsr  17845  mvrf  17851  coe1f2  18019  isphld  18456  pjf  18511  uvcff  18589  frlmup1  18599  cpm2mf  19020  lmbr  19525  tsmsresOLD  20380  tsmsres  20381  prdsdsf  20605  imasdsf1olem  20611  blfps  20644  blf  20645  nmf2  20848  tngngp2  20901  nmof  20961  cphnmf  21377  rrxmet  21570  ovolctb  21636  uniioombllem2  21727  mbfi1fseqlem3  21859  itg2monolem1  21892  itg2monolem2  21893  itg2monolem3  21894  itg2mono  21895  itg2cnlem1  21903  dvres  22050  dvres3a  22053  dvnff  22061  dvcmulf  22083  dvmptcl  22097  dvmptco  22110  dvlipcn  22130  dvgt0lem1  22138  dvle  22143  itgsubstlem  22184  dgrlem  22361  taylpf  22495  taylthlem1  22502  ulmval  22509  ulmshftlem  22518  ulmshft  22519  ulmdvlem1  22529  psergf  22541  pserdvlem2  22557  lgsfcl3  23320  midf  23819  lmif  23828  vdgrf  24574  vdgrfif  24575  grpodivf  24924  nvmf  25217  imsdf  25271  ipf  25302  0oo  25380  hoaddcl  26353  homulcl  26354  hosubcl  26368  brafn  26542  kbop  26548  off2  27154  fmpt3d  27168  fmptcof2  27174  ofoprabco  27177  fpwrelmap  27228  indf1ofs  27679  fibp1  27980  ccatmulgnn0dir  28136  signstf  28163  cvmliftlem6  28375  cvmliftlem10  28379  ftc1anclem3  29669  tailf  29796  rrnmet  29928  pw2f1ocnv  30583  itgpowd  30787  seff  30792  expgrowth  30840  feq1dd  31020  cncficcgt0  31227  fperdvper  31248  itgsubsticclem  31293  itgsbtaddcnst  31300  stoweidlem34  31334  stoweidlem42  31342  stoweidlem48  31348  dirkerf  31397  fourierdlem41  31448  fourierdlem51  31458  fourierdlem57  31464  fourierdlem73  31480  fourierdlem75  31482  fourierdlem103  31510  fourierdlem104  31511  fourierdlem113  31520  tendoplcl  35577  tendoicl  35592
  Copyright terms: Public domain W3C validator