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

Theorem feq1d 5520
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 5516 . 2  |-  ( F  =  G  ->  ( F : A --> B  <->  G : A
--> B ) )
31, 2syl 16 1  |-  ( ph  ->  ( F : A --> B 
<->  G : A --> B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1649   -->wf 5390
This theorem is referenced by:  feq12d  5522  fco2  5541  fssres2  5551  fresin  5552  fresaun  5554  fmptco  5840  fressnfv  5859  off  6259  caofinvl  6270  curry1f  6379  curry2f  6381  eroprf  6938  pmresg  6977  pw2f1olem  7148  ordtypelem4  7423  fseqenlem1  7838  canthp1lem2  8461  fseq1p1m1  11052  s1cl  11682  rlimres  12279  lo1res  12280  rpnnen2lem2  12742  1arithlem3  13220  vdwapf  13267  mrcf  13761  cofucl  14012  funcres  14020  homaf  14112  1stfcl  14221  2ndfcl  14222  prfcl  14227  evlfcl  14246  curf1cl  14252  yonedalem4c  14301  vrmdf  14730  pj1f  15256  efgtf  15281  vrgpf  15327  gsumzres  15444  lspf  15977  psrass1lem  16369  subrgpsr  16409  mvrf  16415  coe1f2  16534  isphld  16808  pjf  16863  lmbr  17244  tsmsres  18094  prdsdsf  18305  imasdsf1olem  18311  blf  18335  nmf2  18511  tngngp2  18564  nmof  18624  cphnmf  19029  ovolctb  19253  uniioombllem2  19342  mbfi1fseqlem3  19476  itg2monolem1  19509  itg2monolem2  19510  itg2monolem3  19511  itg2mono  19512  itg2cnlem1  19520  dvres  19665  dvres3a  19668  dvnff  19676  dvcmulf  19698  dvmptcl  19712  dvmptco  19725  dvlipcn  19745  dvgt0lem1  19753  dvle  19758  itgsubstlem  19799  dgrlem  20015  taylpf  20149  taylthlem1  20156  ulmval  20163  ulmshftlem  20172  ulmshft  20173  ulmdvlem1  20183  psergf  20195  pserdvlem2  20211  lgsfcl3  20968  vdgrf  21517  vdgrfif  21518  grpodivf  21682  nvmf  21975  imsdf  22029  ipf  22060  0oo  22138  hoaddcl  23109  homulcl  23110  hosubcl  23124  brafn  23298  kbop  23304  off2  23897  fmpt3d  23912  fmptcof2  23918  ofoprabco  23921  indf1ofs  24219  cvmliftlem6  24756  cvmliftlem10  24760  tailf  26095  rrnmet  26229  pw2f1ocnv  26799  uvcff  26909  frlmup1  26919  pmtrf  27066  pmtrfinv  27071  pmtrff1o  27073  pmtrfcnv  27074  psgnunilem5  27086  seff  27207  expgrowth  27221  stoweidlem34  27451  stoweidlem42  27459  stoweidlem48  27465  tendoplcl  30895  tendoicl  30910
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-rab 2658  df-v 2901  df-dif 3266  df-un 3268  df-in 3270  df-ss 3277  df-nul 3572  df-if 3683  df-sn 3763  df-pr 3764  df-op 3766  df-br 4154  df-opab 4208  df-rel 4825  df-cnv 4826  df-co 4827  df-dm 4828  df-rn 4829  df-fun 5396  df-fn 5397  df-f 5398
  Copyright terms: Public domain W3C validator