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

Theorem feq1d 5699
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 5695 . 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 1398   -->wf 5566
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rab 2813  df-v 3108  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-br 4440  df-opab 4498  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-fun 5572  df-fn 5573  df-f 5574
This theorem is referenced by:  feq12d  5702  fco2  5724  fssres2  5735  fresin  5736  fresaun  5738  fmptco  6040  fressnfv  6061  off  6527  caofinvl  6540  curry1f  6867  curry2f  6869  f2ndf  6879  eroprf  7401  pmresg  7439  pw2f1olem  7614  ordtypelem4  7938  fseqenlem1  8396  canthp1lem2  9020  fseq1p1m1  11756  repsf  12736  rlimres  13463  lo1res  13464  rpnnen2lem2  14033  1arithlem3  14527  vdwapf  14574  fsets  14744  mrcf  15098  cofucl  15376  funcres  15384  homaf  15508  funcestrcsetclem3  15610  funcestrcsetclem9  15616  funcsetcestrclem3  15624  1stfcl  15665  2ndfcl  15666  prfcl  15671  evlfcl  15690  curf1cl  15696  yonedalem4c  15745  vrmdf  16225  pmtrf  16679  pmtrfinv  16685  pmtrff1o  16687  pmtrfcnv  16688  psgnunilem5  16718  pj1f  16914  efgtf  16939  vrgpf  16985  gsumzres  17113  gsumzresOLD  17117  gsummptfsadd  17139  gsummptfsaddOLD  17140  gsummptfssub  17172  lspf  17815  psrass1lem  18224  subrgpsr  18269  mvrf  18275  coe1f2  18443  isphld  18862  pjf  18917  uvcff  18993  frlmup1  19000  cpm2mf  19420  lmbr  19926  tsmsresOLD  20811  tsmsres  20812  prdsdsf  21036  imasdsf1olem  21042  blfps  21075  blf  21076  nmf2  21279  tngngp2  21332  nmof  21392  cphnmf  21808  rrxmet  22001  ovolctb  22067  uniioombllem2  22158  mbfi1fseqlem3  22290  itg2monolem1  22323  itg2monolem2  22324  itg2monolem3  22325  itg2mono  22326  itg2cnlem1  22334  dvres  22481  dvres3a  22484  dvnff  22492  dvcmulf  22514  dvmptcl  22528  dvmptco  22541  dvlipcn  22561  dvgt0lem1  22569  dvle  22574  itgsubstlem  22615  dgrlem  22792  taylpf  22927  taylthlem1  22934  ulmval  22941  ulmshftlem  22950  ulmshft  22951  ulmdvlem1  22961  psergf  22973  pserdvlem2  22989  logbf  23328  lgsfcl3  23790  midf  24343  lmif  24352  vdgrf  25100  vdgrfif  25101  grpodivf  25446  nvmf  25739  imsdf  25793  ipf  25824  0oo  25902  hoaddcl  26875  homulcl  26876  hosubcl  26890  brafn  27064  kbop  27070  off2  27702  fmpt3d  27717  fmptcof2  27724  ofoprabco  27732  fpwrelmap  27787  indf1ofs  28255  fibp1  28604  ccatmulgnn0dir  28760  cvmliftlem6  28999  cvmliftlem10  29003  mrsubff  29136  msubff  29154  ftc1anclem3  30332  tailf  30433  rrnmet  30565  pw2f1ocnv  31218  itgpowd  31423  seff  31430  expgrowth  31481  feq1dd  31682  dvnmul  31979  dvnprodlem2  31983  dvnprodlem3  31984  stoweidlem34  32055  stoweidlem42  32063  stoweidlem48  32069  dirkerf  32118  fourierdlem41  32169  fourierdlem51  32179  fourierdlem57  32185  fourierdlem60  32188  fourierdlem61  32189  fourierdlem73  32201  fourierdlem75  32203  fourierdlem103  32231  fourierdlem104  32232  etransclem1  32257  etransclem2  32258  etransclem20  32276  etransclem33  32289  etransclem46  32302  pfxf  32617  funcringcsetcALTV2lem3  33100  funcringcsetcALTV2lem9  33106  funcringcsetclem3ALTV  33123  funcringcsetclem9ALTV  33129  fdivmptf  33416  refdivmptf  33417  tendoplcl  36904  tendoicl  36919
  Copyright terms: Public domain W3C validator