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

Theorem feq1d 5668
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 5664 . 2  |-  ( F  =  G  ->  ( F : A --> B  <->  G : A
--> B ) )
31, 2syl 17 1  |-  ( ph  ->  ( F : A --> B 
<->  G : A --> B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    = wceq 1437   -->wf 5533
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2402
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2552  df-rab 2717  df-v 3018  df-dif 3375  df-un 3377  df-in 3379  df-ss 3386  df-nul 3698  df-if 3848  df-sn 3935  df-pr 3937  df-op 3941  df-br 4360  df-opab 4419  df-rel 4796  df-cnv 4797  df-co 4798  df-dm 4799  df-rn 4800  df-fun 5539  df-fn 5540  df-f 5541
This theorem is referenced by:  feq12d  5671  fco2  5693  fssres2  5704  fresin  5705  fresaun  5707  fmpt3d  5999  fmptco  6008  fressnfv  6030  off  6497  caofinvl  6509  curry1f  6838  curry2f  6840  f2ndf  6850  eroprf  7409  pmresg  7447  pw2f1olem  7622  ordtypelem4  7982  fseqenlem1  8399  canthp1lem2  9022  fseq1p1m1  11812  repsf  12815  rlimres  13558  lo1res  13559  rpnnen2lem2  14204  1arithlem3  14805  vdwapf  14858  fsets  15085  mrcf  15451  cofucl  15729  funcres  15737  homaf  15861  funcestrcsetclem3  15963  funcestrcsetclem9  15969  funcsetcestrclem3  15977  1stfcl  16018  2ndfcl  16019  prfcl  16024  evlfcl  16043  curf1cl  16049  yonedalem4c  16098  vrmdf  16578  pmtrf  17032  pmtrfinv  17038  pmtrff1o  17040  pmtrfcnv  17041  psgnunilem5  17071  pj1f  17283  efgtf  17308  vrgpf  17354  gsumzres  17479  gsummptfsadd  17493  gsummptfssub  17518  lspf  18133  psrass1lem  18537  subrgpsr  18579  mvrf  18584  coe1f2  18738  isphld  19156  pjf  19211  uvcff  19284  frlmup1  19291  cpm2mf  19711  lmbr  20209  tsmsres  21093  prdsdsf  21317  imasdsf1olem  21323  blfps  21356  blf  21357  nmf2  21542  tngngp2  21595  nmofOLD  21677  cphnmf  22108  rrxmet  22297  ovolctb  22378  uniioombllem2  22475  uniioombllem2OLD  22476  mbfi1fseqlem3  22610  itg2monolem1  22643  itg2monolem2  22644  itg2monolem3  22645  itg2mono  22646  itg2cnlem1  22654  dvres  22801  dvres3a  22804  dvnff  22812  dvcmulf  22834  dvmptcl  22848  dvmptco  22861  dvlipcn  22881  dvgt0lem1  22889  dvle  22894  itgsubstlem  22935  dgrlem  23118  taylpf  23256  taylthlem1  23263  ulmval  23270  ulmshftlem  23279  ulmshft  23280  ulmdvlem1  23290  psergf  23302  pserdvlem2  23318  logbf  23661  lgsfcl3  24180  midf  24753  lmif  24762  vdgrf  25561  vdgrfif  25562  grpodivf  25909  nvmf  26202  imsdf  26256  ipf  26287  0oo  26365  hoaddcl  27346  homulcl  27347  hosubcl  27361  brafn  27535  kbop  27541  off2  28181  fmptcof2  28198  ofoprabco  28206  fpwrelmap  28261  indf1ofs  28792  sitmf  29130  fibp1  29179  ccatmulgnn0dir  29373  cvmliftlem6  29958  cvmliftlem10  29962  mrsubff  30095  msubff  30113  tailf  30973  poimirlem24  31865  ftc1anclem3  31920  rrnmet  32062  tendoplcl  34254  tendoicl  34269  pw2f1ocnv  35799  itgpowd  36006  seff  36564  expgrowth  36591  feq1dd  37327  dvnmul  37695  dvnprodlem2  37699  dvnprodlem3  37700  stoweidlem34  37772  stoweidlem42  37780  stoweidlem48  37786  dirkerf  37836  fourierdlem41  37888  fourierdlem51  37898  fourierdlem57  37904  fourierdlem60  37907  fourierdlem61  37908  fourierdlem73  37920  fourierdlem75  37922  fourierdlem103  37950  fourierdlem104  37951  etransclem1  37977  etransclem2  37978  etransclem20  37996  etransclem33  38009  etransclem46  38022  sge0isum  38114  isomenndlem  38196  hoicvr  38211  ovnf  38226  ovnsubaddlem1  38233  hsphoif  38239  hoidmvlelem2  38259  hoidmvlelem3  38260  ovnhoilem1  38264  ovnhoilem2  38265  pfxf  38737  funcringcsetcALTV2lem3  39625  funcringcsetcALTV2lem9  39631  funcringcsetclem3ALTV  39648  funcringcsetclem9ALTV  39654  fdivmptf  39939  refdivmptf  39940
  Copyright terms: Public domain W3C validator