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

Theorem feq1d 5997
Description: Equality deduction for functions. (Contributed by NM, 19-Feb-2008.)
Hypothesis
Ref Expression
feq1d.1 (𝜑𝐹 = 𝐺)
Assertion
Ref Expression
feq1d (𝜑 → (𝐹:𝐴𝐵𝐺:𝐴𝐵))

Proof of Theorem feq1d
StepHypRef Expression
1 feq1d.1 . 2 (𝜑𝐹 = 𝐺)
2 feq1 5993 . 2 (𝐹 = 𝐺 → (𝐹:𝐴𝐵𝐺:𝐴𝐵))
31, 2syl 17 1 (𝜑 → (𝐹:𝐴𝐵𝐺:𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1480  wf 5853
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-rab 2917  df-v 3192  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3898  df-if 4065  df-sn 4156  df-pr 4158  df-op 4162  df-br 4624  df-opab 4684  df-rel 5091  df-cnv 5092  df-co 5093  df-dm 5094  df-rn 5095  df-fun 5859  df-fn 5860  df-f 5861
This theorem is referenced by:  feq12d  6000  fco2  6026  fssres2  6039  fresin  6040  fresaun  6042  fmpt3d  6352  fressnfv  6392  off  6877  caofinvl  6889  curry1f  7231  curry2f  7233  f2ndf  7243  eroprf  7805  pmresg  7845  pw2f1olem  8024  ordtypelem4  8386  fseqenlem1  8807  canthp1lem2  9435  fseq1p1m1  12371  repsf  13473  rlimres  14239  lo1res  14240  rpnnen2lem2  14888  1arithlem3  15572  vdwapf  15619  fsets  15831  mrcf  16209  cofucl  16488  funcres  16496  homaf  16620  funcestrcsetclem3  16722  funcestrcsetclem9  16728  funcsetcestrclem3  16736  1stfcl  16777  2ndfcl  16778  prfcl  16783  evlfcl  16802  curf1cl  16808  yonedalem4c  16857  vrmdf  17335  pmtrf  17815  pmtrfinv  17821  pmtrff1o  17823  pmtrfcnv  17824  psgnunilem5  17854  pj1f  18050  efgtf  18075  vrgpf  18121  gsumzres  18250  gsummptfsadd  18264  gsummptfssub  18289  lspf  18914  psrass1lem  19317  subrgpsr  19359  mvrf  19364  coe1f2  19519  isphld  19939  pjf  19997  uvcff  20070  frlmup1  20077  cpm2mf  20497  lmbr  21002  tsmsres  21887  prdsdsf  22112  imasdsf1olem  22118  blfps  22151  blf  22152  nmf2  22337  tngngp2  22396  cphnmf  22935  rrxmet  23131  ovolctb  23198  uniioombllem2  23291  mbfi1fseqlem3  23424  itg2monolem1  23457  itg2monolem2  23458  itg2monolem3  23459  itg2mono  23460  itg2cnlem1  23468  dvres  23615  dvres3a  23618  dvnff  23626  dvcmulf  23648  dvmptcl  23662  dvmptco  23675  dvlipcn  23695  dvgt0lem1  23703  dvle  23708  itgsubstlem  23749  dgrlem  23923  taylpf  24058  taylthlem1  24065  ulmval  24072  ulmshftlem  24081  ulmshft  24082  ulmdvlem1  24092  psergf  24104  pserdvlem2  24120  logbf  24461  lgsfcl3  24977  midf  25602  lmif  25611  vtxdgf  26287  grpodivf  27280  nvmf  27388  imsdf  27432  ipf  27456  0oo  27532  hoaddcl  28505  homulcl  28506  hosubcl  28520  brafn  28694  kbop  28700  off2  29326  fmptcof2  29340  ofoprabco  29348  fpwrelmap  29392  indf1ofs  29911  sitmf  30237  fibp1  30286  ccatmulgnn0dir  30441  breprsuc  30501  cvmliftlem6  31033  cvmliftlem10  31037  mrsubff  31170  msubff  31188  tailf  32065  curf  33058  uncf  33059  poimirlem24  33104  ftc1anclem3  33158  rrnmet  33299  tendoplcl  35588  tendoicl  35603  pw2f1ocnv  37123  itgpowd  37320  seff  38029  expgrowth  38055  feq1dd  38856  dvnmul  39495  dvnprodlem2  39499  dvnprodlem3  39500  voliooicof  39550  stoweidlem34  39588  stoweidlem42  39596  stoweidlem48  39602  dirkerf  39651  fourierdlem41  39702  fourierdlem51  39711  fourierdlem57  39717  fourierdlem60  39720  fourierdlem61  39721  fourierdlem73  39733  fourierdlem75  39735  fourierdlem103  39763  fourierdlem104  39764  etransclem1  39789  etransclem2  39790  etransclem20  39808  etransclem33  39821  etransclem46  39834  sge0isum  39981  sge0seq  40000  isomenndlem  40081  hoicvr  40099  ovnf  40114  ovnsubaddlem1  40121  hsphoif  40127  hoidmvlelem2  40147  hoidmvlelem3  40148  ovnhoilem1  40152  ovnhoilem2  40153  ovncvr2  40162  hoidifhspf  40169  hspmbllem2  40178  iccvonmbllem  40229  vonioolem1  40231  vonioolem2  40232  vonicclem1  40234  vonicclem2  40235  pfxf  40718  1hegrlfgr  41031  funcringcsetcALTV2lem3  41356  funcringcsetcALTV2lem9  41362  funcringcsetclem3ALTV  41379  funcringcsetclem9ALTV  41385  fdivmptf  41657  refdivmptf  41658
  Copyright terms: Public domain W3C validator