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

Theorem feq1d 6492
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 6488 . 2 (𝐹 = 𝐺 → (𝐹:𝐴𝐵𝐺:𝐴𝐵))
31, 2syl 17 1 (𝜑 → (𝐹:𝐴𝐵𝐺:𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207   = wceq 1528  wf 6344
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-br 5058  df-opab 5120  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-fun 6350  df-fn 6351  df-f 6352
This theorem is referenced by:  feq12d  6495  fco2  6526  fssres2  6539  fresin  6540  fresaun  6542  fmpt3d  6872  fressnfv  6914  f2ndf  7805  eroprf  8384  pmresg  8423  pw2f1olem  8609  ordtypelem4  8973  canthp1lem2  10063  fseq1p1m1  12969  repsf  14123  rlimres  14903  lo1res  14904  vdwapf  16296  fsets  16504  mrcf  16868  cofucl  17146  funcres  17154  funcestrcsetclem9  17386  1stfcl  17435  2ndfcl  17436  evlfcl  17460  yonedalem4c  17515  pmtrfinv  18518  pmtrff1o  18520  pmtrfcnv  18521  efgtf  18777  gsumzres  18958  psrass1lem  20085  coe1f2  20305  isphld  20726  pjf  20785  frlmup1  20870  lmbr  21794  tsmsres  22679  prdsdsf  22904  imasdsf1olem  22910  blfps  22943  blf  22944  tngngp2  23188  rrxmet  23938  ovolctb  24018  itg2monolem1  24278  itg2monolem2  24279  itg2monolem3  24280  itg2mono  24281  dvres  24436  dvres3a  24439  dvnff  24447  dvcmulf  24469  dvmptcl  24483  dvmptco  24496  dvlipcn  24518  dvgt0lem1  24526  itgsubstlem  24572  dgrlem  24746  taylthlem1  24888  ulmval  24895  lgsfcl3  25821  midf  26489  grpodivf  28242  nvmf  28349  imsdf  28393  ipf  28417  0oo  28493  hoaddcl  29462  homulcl  29463  hosubcl  29477  fmptcof2  30330  ofoprabco  30337  fpwrelmap  30395  fedgmullem1  30924  indf1ofs  31184  sitmf  31509  fibp1  31558  ccatmulgnn0dir  31711  reprsuc  31785  pfxwlk  32267  cvmliftlem6  32434  cvmliftlem10  32438  mrsubff  32656  msubff  32674  tailf  33620  curf  34751  uncf  34752  poimirlem24  34797  ftc1anclem3  34850  rrnmet  34988  tendoplcl  37797  tendoicl  37812  pw2f1ocnv  39512  itgpowd  39699  seff  40518  expgrowth  40544  feq1dd  41299  dvnmul  42104  dvnprodlem2  42108  dvnprodlem3  42109  voliooicof  42158  stoweidlem34  42196  stoweidlem42  42204  stoweidlem48  42210  dirkerf  42259  fourierdlem41  42310  fourierdlem51  42319  fourierdlem57  42325  fourierdlem60  42328  fourierdlem61  42329  fourierdlem73  42341  fourierdlem75  42343  fourierdlem103  42371  fourierdlem104  42372  etransclem1  42397  etransclem2  42398  etransclem20  42416  etransclem33  42429  etransclem46  42442  sge0isum  42586  sge0seq  42605  isomenndlem  42689  hoicvr  42707  ovnf  42722  ovnsubaddlem1  42729  hsphoif  42735  hoidmvlelem2  42755  hoidmvlelem3  42756  ovnhoilem1  42760  ovnhoilem2  42761  ovncvr2  42770  hoidifhspf  42777  hspmbllem2  42786  iccvonmbllem  42837  vonioolem1  42839  vonioolem2  42840  vonicclem1  42842  vonicclem2  42843  1hegrlfgr  43884  funcringcsetcALTV2lem3  44237  funcringcsetcALTV2lem9  44243  funcringcsetclem3ALTV  44260  funcringcsetclem9ALTV  44266  fdivmptf  44529  refdivmptf  44530
  Copyright terms: Public domain W3C validator