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

Theorem feq1d 5736
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 5732 . 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 189    = wceq 1455   -->wf 5597
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-rab 2758  df-v 3059  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-br 4417  df-opab 4476  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-fun 5603  df-fn 5604  df-f 5605
This theorem is referenced by:  feq12d  5739  fco2  5763  fssres2  5774  fresin  5775  fresaun  5777  fmpt3d  6070  fmptco  6080  fressnfv  6102  off  6573  caofinvl  6585  curry1f  6917  curry2f  6919  f2ndf  6929  eroprf  7487  pmresg  7525  pw2f1olem  7702  ordtypelem4  8062  fseqenlem1  8481  canthp1lem2  9104  fseq1p1m1  11897  repsf  12913  rlimres  13671  lo1res  13672  rpnnen2lem2  14317  1arithlem3  14918  vdwapf  14971  fsets  15198  mrcf  15564  cofucl  15842  funcres  15850  homaf  15974  funcestrcsetclem3  16076  funcestrcsetclem9  16082  funcsetcestrclem3  16090  1stfcl  16131  2ndfcl  16132  prfcl  16137  evlfcl  16156  curf1cl  16162  yonedalem4c  16211  vrmdf  16691  pmtrf  17145  pmtrfinv  17151  pmtrff1o  17153  pmtrfcnv  17154  psgnunilem5  17184  pj1f  17396  efgtf  17421  vrgpf  17467  gsumzres  17592  gsummptfsadd  17606  gsummptfssub  17631  lspf  18246  psrass1lem  18650  subrgpsr  18692  mvrf  18697  coe1f2  18851  isphld  19270  pjf  19325  uvcff  19398  frlmup1  19405  cpm2mf  19825  lmbr  20323  tsmsres  21207  prdsdsf  21431  imasdsf1olem  21437  blfps  21470  blf  21471  nmf2  21656  tngngp2  21709  nmofOLD  21791  cphnmf  22222  rrxmet  22411  ovolctb  22492  uniioombllem2  22589  uniioombllem2OLD  22590  mbfi1fseqlem3  22724  itg2monolem1  22757  itg2monolem2  22758  itg2monolem3  22759  itg2mono  22760  itg2cnlem1  22768  dvres  22915  dvres3a  22918  dvnff  22926  dvcmulf  22948  dvmptcl  22962  dvmptco  22975  dvlipcn  22995  dvgt0lem1  23003  dvle  23008  itgsubstlem  23049  dgrlem  23232  taylpf  23370  taylthlem1  23377  ulmval  23384  ulmshftlem  23393  ulmshft  23394  ulmdvlem1  23404  psergf  23416  pserdvlem2  23432  logbf  23775  lgsfcl3  24294  midf  24867  lmif  24876  vdgrf  25675  vdgrfif  25676  grpodivf  26023  nvmf  26316  imsdf  26370  ipf  26401  0oo  26479  hoaddcl  27460  homulcl  27461  hosubcl  27475  brafn  27649  kbop  27655  off2  28291  fmptcof2  28308  ofoprabco  28316  fpwrelmap  28367  indf1ofs  28896  sitmf  29234  fibp1  29283  ccatmulgnn0dir  29477  cvmliftlem6  30062  cvmliftlem10  30066  mrsubff  30199  msubff  30217  tailf  31080  poimirlem24  32009  ftc1anclem3  32064  rrnmet  32206  tendoplcl  34393  tendoicl  34408  pw2f1ocnv  35937  itgpowd  36144  seff  36701  expgrowth  36728  feq1dd  37468  dvnmul  37856  dvnprodlem2  37860  dvnprodlem3  37861  stoweidlem34  37933  stoweidlem42  37941  stoweidlem48  37947  dirkerf  37997  fourierdlem41  38049  fourierdlem51  38059  fourierdlem57  38065  fourierdlem60  38068  fourierdlem61  38069  fourierdlem73  38081  fourierdlem75  38083  fourierdlem103  38111  fourierdlem104  38112  etransclem1  38138  etransclem2  38139  etransclem20  38157  etransclem33  38170  etransclem46  38183  sge0isum  38307  isomenndlem  38389  hoicvr  38408  ovnf  38423  ovnsubaddlem1  38430  hsphoif  38436  hoidmvlelem2  38456  hoidmvlelem3  38457  ovnhoilem1  38461  ovnhoilem2  38462  ovncvr2  38471  hoidifhspf  38478  hspmbllem2  38487  pfxf  38970  vtxdgf  39581  funcringcsetcALTV2lem3  40313  funcringcsetcALTV2lem9  40319  funcringcsetclem3ALTV  40336  funcringcsetclem9ALTV  40342  fdivmptf  40625  refdivmptf  40626
  Copyright terms: Public domain W3C validator