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

Theorem feq1d 5925
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 5921 . 2 (𝐹 = 𝐺 → (𝐹:𝐴𝐵𝐺:𝐴𝐵))
31, 2syl 17 1 (𝜑 → (𝐹:𝐴𝐵𝐺:𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194   = wceq 1474  wf 5782
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-rab 2900  df-v 3170  df-dif 3538  df-un 3540  df-in 3542  df-ss 3549  df-nul 3870  df-if 4032  df-sn 4121  df-pr 4123  df-op 4127  df-br 4574  df-opab 4634  df-rel 5031  df-cnv 5032  df-co 5033  df-dm 5034  df-rn 5035  df-fun 5788  df-fn 5789  df-f 5790
This theorem is referenced by:  feq12d  5928  fco2  5954  fssres2  5966  fresin  5967  fresaun  5969  fmpt3d  6274  fressnfv  6306  off  6783  caofinvl  6795  curry1f  7131  curry2f  7133  f2ndf  7143  eroprf  7705  pmresg  7744  pw2f1olem  7922  ordtypelem4  8282  fseqenlem1  8703  canthp1lem2  9327  fseq1p1m1  12234  repsf  13313  rlimres  14079  lo1res  14080  rpnnen2lem2  14725  1arithlem3  15409  vdwapf  15456  fsets  15665  mrcf  16034  cofucl  16313  funcres  16321  homaf  16445  funcestrcsetclem3  16547  funcestrcsetclem9  16553  funcsetcestrclem3  16561  1stfcl  16602  2ndfcl  16603  prfcl  16608  evlfcl  16627  curf1cl  16633  yonedalem4c  16682  vrmdf  17160  pmtrf  17640  pmtrfinv  17646  pmtrff1o  17648  pmtrfcnv  17649  psgnunilem5  17679  pj1f  17875  efgtf  17900  vrgpf  17946  gsumzres  18075  gsummptfsadd  18089  gsummptfssub  18114  lspf  18737  psrass1lem  19140  subrgpsr  19182  mvrf  19187  coe1f2  19342  isphld  19759  pjf  19814  uvcff  19887  frlmup1  19894  cpm2mf  20314  lmbr  20810  tsmsres  21695  prdsdsf  21919  imasdsf1olem  21925  blfps  21958  blf  21959  nmf2  22144  tngngp2  22200  cphnmf  22723  rrxmet  22912  ovolctb  22978  uniioombllem2  23070  mbfi1fseqlem3  23203  itg2monolem1  23236  itg2monolem2  23237  itg2monolem3  23238  itg2mono  23239  itg2cnlem1  23247  dvres  23394  dvres3a  23397  dvnff  23405  dvcmulf  23427  dvmptcl  23441  dvmptco  23454  dvlipcn  23474  dvgt0lem1  23482  dvle  23487  itgsubstlem  23528  dgrlem  23702  taylpf  23837  taylthlem1  23844  ulmval  23851  ulmshftlem  23860  ulmshft  23861  ulmdvlem1  23871  psergf  23883  pserdvlem2  23899  logbf  24240  lgsfcl3  24756  midf  25382  lmif  25391  vdgrf  26187  vdgrfif  26188  grpodivf  26538  nvmf  26667  imsdf  26721  ipf  26752  0oo  26830  hoaddcl  27803  homulcl  27804  hosubcl  27818  brafn  27992  kbop  27998  off2  28625  fmptcof2  28641  ofoprabco  28649  fpwrelmap  28698  indf1ofs  29217  sitmf  29543  fibp1  29592  ccatmulgnn0dir  29747  cvmliftlem6  30328  cvmliftlem10  30332  mrsubff  30465  msubff  30483  tailf  31342  curf  32356  uncf  32357  poimirlem24  32402  ftc1anclem3  32456  rrnmet  32597  tendoplcl  34886  tendoicl  34901  pw2f1ocnv  36421  itgpowd  36618  seff  37329  expgrowth  37355  feq1dd  38140  dvnmul  38633  dvnprodlem2  38637  dvnprodlem3  38638  voliooicof  38689  stoweidlem34  38727  stoweidlem42  38735  stoweidlem48  38741  dirkerf  38790  fourierdlem41  38841  fourierdlem51  38850  fourierdlem57  38856  fourierdlem60  38859  fourierdlem61  38860  fourierdlem73  38872  fourierdlem75  38874  fourierdlem103  38902  fourierdlem104  38903  etransclem1  38928  etransclem2  38929  etransclem20  38947  etransclem33  38960  etransclem46  38973  sge0isum  39120  sge0seq  39139  isomenndlem  39220  hoicvr  39238  ovnf  39253  ovnsubaddlem1  39260  hsphoif  39266  hoidmvlelem2  39286  hoidmvlelem3  39287  ovnhoilem1  39291  ovnhoilem2  39292  ovncvr2  39301  hoidifhspf  39308  hspmbllem2  39317  iccvonmbllem  39369  vonioolem1  39371  vonioolem2  39372  vonicclem1  39374  vonicclem2  39375  pfxf  40053  vtxdgf  40684  1hegrlfgr  40720  funcringcsetcALTV2lem3  41828  funcringcsetcALTV2lem9  41834  funcringcsetclem3ALTV  41851  funcringcsetclem9ALTV  41857  fdivmptf  42131  refdivmptf  42132
  Copyright terms: Public domain W3C validator