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

Theorem feq1d 5707
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 5703 . 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 1383   -->wf 5574
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-rab 2802  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-br 4438  df-opab 4496  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-fun 5580  df-fn 5581  df-f 5582
This theorem is referenced by:  feq12d  5710  fco2  5732  fssres2  5743  fresin  5744  fresaun  5746  fmptco  6049  fressnfv  6070  off  6539  caofinvl  6552  curry1f  6879  curry2f  6881  f2ndf  6891  eroprf  7411  pmresg  7448  pw2f1olem  7623  ordtypelem4  7949  fseqenlem1  8408  canthp1lem2  9034  fseq1p1m1  11761  repsf  12724  rlimres  13360  lo1res  13361  rpnnen2lem2  13826  1arithlem3  14320  vdwapf  14367  fsets  14535  mrcf  14883  cofucl  15131  funcres  15139  homaf  15231  1stfcl  15340  2ndfcl  15341  prfcl  15346  evlfcl  15365  curf1cl  15371  yonedalem4c  15420  vrmdf  15900  pmtrf  16354  pmtrfinv  16360  pmtrff1o  16362  pmtrfcnv  16363  psgnunilem5  16393  pj1f  16589  efgtf  16614  vrgpf  16660  gsumzres  16788  gsumzresOLD  16792  gsummptfsadd  16814  gsummptfsaddOLD  16815  gsummptfssub  16850  lspf  17494  psrass1lem  17903  subrgpsr  17948  mvrf  17954  coe1f2  18122  isphld  18562  pjf  18617  uvcff  18695  frlmup1  18705  cpm2mf  19126  lmbr  19632  tsmsresOLD  20518  tsmsres  20519  prdsdsf  20743  imasdsf1olem  20749  blfps  20782  blf  20783  nmf2  20986  tngngp2  21039  nmof  21099  cphnmf  21515  rrxmet  21708  ovolctb  21774  uniioombllem2  21865  mbfi1fseqlem3  21997  itg2monolem1  22030  itg2monolem2  22031  itg2monolem3  22032  itg2mono  22033  itg2cnlem1  22041  dvres  22188  dvres3a  22191  dvnff  22199  dvcmulf  22221  dvmptcl  22235  dvmptco  22248  dvlipcn  22268  dvgt0lem1  22276  dvle  22281  itgsubstlem  22322  dgrlem  22499  taylpf  22633  taylthlem1  22640  ulmval  22647  ulmshftlem  22656  ulmshft  22657  ulmdvlem1  22667  psergf  22679  pserdvlem2  22695  lgsfcl3  23464  midf  24014  lmif  24023  vdgrf  24770  vdgrfif  24771  grpodivf  25120  nvmf  25413  imsdf  25467  ipf  25498  0oo  25576  hoaddcl  26549  homulcl  26550  hosubcl  26564  brafn  26738  kbop  26744  off2  27353  fmpt3d  27368  fmptcof2  27374  ofoprabco  27377  fpwrelmap  27428  indf1ofs  27912  fibp1  28213  ccatmulgnn0dir  28369  cvmliftlem6  28608  cvmliftlem10  28612  mrsubff  28745  msubff  28763  ftc1anclem3  30067  tailf  30168  rrnmet  30300  pw2f1ocnv  30954  itgpowd  31158  seff  31165  expgrowth  31216  feq1dd  31392  stoweidlem34  31705  stoweidlem42  31713  stoweidlem48  31719  dirkerf  31768  fourierdlem41  31819  fourierdlem51  31829  fourierdlem57  31835  fourierdlem60  31838  fourierdlem61  31839  fourierdlem73  31851  fourierdlem75  31853  fourierdlem103  31881  fourierdlem104  31882  funcestrcsetclem3  32497  funcestrcsetclem9  32503  funcringcsetcOLD2lem3  32583  funcringcsetcOLD2lem9  32589  funcringcsetclem3OLD  32606  funcringcsetclem9OLD  32612  tendoplcl  36247  tendoicl  36262
  Copyright terms: Public domain W3C validator