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

Theorem feq1d 5541
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 5537 . 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 1369   -->wf 5409
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rab 2719  df-v 2969  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-br 4288  df-opab 4346  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-fun 5415  df-fn 5416  df-f 5417
This theorem is referenced by:  feq12d  5543  fco2  5564  fssres2  5574  fresin  5575  fresaun  5577  fmptco  5871  fressnfv  5891  off  6329  caofinvl  6342  curry1f  6661  curry2f  6663  f2ndf  6673  eroprf  7190  pmresg  7232  pw2f1olem  7407  ordtypelem4  7727  fseqenlem1  8186  canthp1lem2  8812  fseq1p1m1  11526  repsf  12403  rlimres  13028  lo1res  13029  rpnnen2lem2  13490  1arithlem3  13978  vdwapf  14025  fsets  14192  mrcf  14539  cofucl  14790  funcres  14798  homaf  14890  1stfcl  14999  2ndfcl  15000  prfcl  15005  evlfcl  15024  curf1cl  15030  yonedalem4c  15079  vrmdf  15527  pmtrf  15952  pmtrfinv  15958  pmtrff1o  15960  pmtrfcnv  15961  psgnunilem5  15991  pj1f  16185  efgtf  16210  vrgpf  16256  gsumzres  16379  gsumzresOLD  16383  gsummptfsadd  16405  gsummptfsaddOLD  16406  lspf  17032  psrass1lem  17424  subrgpsr  17468  mvrf  17474  coe1f2  17640  isphld  18058  pjf  18113  uvcff  18191  frlmup1  18201  lmbr  18837  tsmsresOLD  19692  tsmsres  19693  prdsdsf  19917  imasdsf1olem  19923  blfps  19956  blf  19957  nmf2  20160  tngngp2  20213  nmof  20273  cphnmf  20689  rrxmet  20882  ovolctb  20948  uniioombllem2  21038  mbfi1fseqlem3  21170  itg2monolem1  21203  itg2monolem2  21204  itg2monolem3  21205  itg2mono  21206  itg2cnlem1  21214  dvres  21361  dvres3a  21364  dvnff  21372  dvcmulf  21394  dvmptcl  21408  dvmptco  21421  dvlipcn  21441  dvgt0lem1  21449  dvle  21454  itgsubstlem  21495  dgrlem  21672  taylpf  21806  taylthlem1  21813  ulmval  21820  ulmshftlem  21829  ulmshft  21830  ulmdvlem1  21840  psergf  21852  pserdvlem2  21868  lgsfcl3  22631  vdgrf  23519  vdgrfif  23520  grpodivf  23684  nvmf  23977  imsdf  24031  ipf  24062  0oo  24140  hoaddcl  25113  homulcl  25114  hosubcl  25128  brafn  25302  kbop  25308  off2  25910  fmpt3d  25924  fmptcof2  25930  ofoprabco  25933  fpwrelmap  25984  indf1ofs  26434  fibp1  26736  ccatmulgnn0dir  26892  signstf  26919  cvmliftlem6  27131  cvmliftlem10  27135  ftc1anclem3  28422  tailf  28549  rrnmet  28681  pw2f1ocnv  29339  itgpowd  29543  seff  29548  expgrowth  29562  stoweidlem34  29782  stoweidlem42  29790  stoweidlem48  29796  tendoplcl  34265  tendoicl  34280
  Copyright terms: Public domain W3C validator