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

Theorem feq1d 6068
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 6064 . 2 (𝐹 = 𝐺 → (𝐹:𝐴𝐵𝐺:𝐴𝐵))
31, 2syl 17 1 (𝜑 → (𝐹:𝐴𝐵𝐺:𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1523  wf 5922
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-br 4686  df-opab 4746  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-fun 5928  df-fn 5929  df-f 5930
This theorem is referenced by:  feq12d  6071  fco2  6097  fssres2  6110  fresin  6111  fresaun  6113  fmpt3d  6426  fressnfv  6467  off  6954  caofinvl  6966  curry1f  7316  curry2f  7318  f2ndf  7328  eroprf  7888  pmresg  7927  pw2f1olem  8105  ordtypelem4  8467  fseqenlem1  8885  canthp1lem2  9513  fseq1p1m1  12452  repsf  13566  rlimres  14333  lo1res  14334  rpnnen2lem2  14988  1arithlem3  15676  vdwapf  15723  fsets  15938  mrcf  16316  cofucl  16595  funcres  16603  homaf  16727  funcestrcsetclem3  16829  funcestrcsetclem9  16835  funcsetcestrclem3  16843  1stfcl  16884  2ndfcl  16885  prfcl  16890  evlfcl  16909  curf1cl  16915  yonedalem4c  16964  vrmdf  17442  pmtrf  17921  pmtrfinv  17927  pmtrff1o  17929  pmtrfcnv  17930  psgnunilem5  17960  pj1f  18156  efgtf  18181  vrgpf  18227  gsumzres  18356  gsummptfsadd  18370  gsummptfssub  18395  lspf  19022  psrass1lem  19425  subrgpsr  19467  mvrf  19472  coe1f2  19627  isphld  20047  pjf  20105  uvcff  20178  frlmup1  20185  cpm2mf  20605  lmbr  21110  tsmsres  21994  prdsdsf  22219  imasdsf1olem  22225  blfps  22258  blf  22259  nmf2  22444  tngngp2  22503  cphnmf  23041  rrxmet  23237  ovolctb  23304  uniioombllem2  23397  mbfi1fseqlem3  23529  itg2monolem1  23562  itg2monolem2  23563  itg2monolem3  23564  itg2mono  23565  itg2cnlem1  23573  dvres  23720  dvres3a  23723  dvnff  23731  dvcmulf  23753  dvmptcl  23767  dvmptco  23780  dvlipcn  23802  dvgt0lem1  23810  dvle  23815  itgsubstlem  23856  dgrlem  24030  taylpf  24165  taylthlem1  24172  ulmval  24179  ulmshftlem  24188  ulmshft  24189  ulmdvlem1  24199  psergf  24211  pserdvlem2  24227  logbf  24572  lgsfcl3  25088  midf  25713  lmif  25722  vtxdgf  26423  grpodivf  27520  nvmf  27628  imsdf  27672  ipf  27696  0oo  27772  hoaddcl  28745  homulcl  28746  hosubcl  28760  brafn  28934  kbop  28940  off2  29571  fmptcof2  29585  ofoprabco  29592  fpwrelmap  29636  indf1ofs  30216  sitmf  30542  fibp1  30591  ccatmulgnn0dir  30747  reprsuc  30821  cvmliftlem6  31398  cvmliftlem10  31402  mrsubff  31535  msubff  31553  tailf  32495  curf  33517  uncf  33518  poimirlem24  33563  ftc1anclem3  33617  rrnmet  33758  tendoplcl  36386  tendoicl  36401  pw2f1ocnv  37921  itgpowd  38117  seff  38825  expgrowth  38851  feq1dd  39661  dvnmul  40476  dvnprodlem2  40480  dvnprodlem3  40481  voliooicof  40531  stoweidlem34  40569  stoweidlem42  40577  stoweidlem48  40583  dirkerf  40632  fourierdlem41  40683  fourierdlem51  40692  fourierdlem57  40698  fourierdlem60  40701  fourierdlem61  40702  fourierdlem73  40714  fourierdlem75  40716  fourierdlem103  40744  fourierdlem104  40745  etransclem1  40770  etransclem2  40771  etransclem20  40789  etransclem33  40802  etransclem46  40815  sge0isum  40962  sge0seq  40981  isomenndlem  41065  hoicvr  41083  ovnf  41098  ovnsubaddlem1  41105  hsphoif  41111  hoidmvlelem2  41131  hoidmvlelem3  41132  ovnhoilem1  41136  ovnhoilem2  41137  ovncvr2  41146  hoidifhspf  41153  hspmbllem2  41162  iccvonmbllem  41213  vonioolem1  41215  vonioolem2  41216  vonicclem1  41218  vonicclem2  41219  pfxf  41714  1hegrlfgr  42038  funcringcsetcALTV2lem3  42363  funcringcsetcALTV2lem9  42369  funcringcsetclem3ALTV  42386  funcringcsetclem9ALTV  42392  fdivmptf  42660  refdivmptf  42661
  Copyright terms: Public domain W3C validator