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

Theorem feq1i 6478
Description: Equality inference for functions. (Contributed by Paul Chapman, 22-Jun-2011.)
Hypothesis
Ref Expression
feq1i.1 𝐹 = 𝐺
Assertion
Ref Expression
feq1i (𝐹:𝐴𝐵𝐺:𝐴𝐵)

Proof of Theorem feq1i
StepHypRef Expression
1 feq1i.1 . 2 𝐹 = 𝐺
2 feq1 6468 . 2 (𝐹 = 𝐺 → (𝐹:𝐴𝐵𝐺:𝐴𝐵))
31, 2ax-mp 5 1 (𝐹:𝐴𝐵𝐺:𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 209   = wceq 1538  wf 6324
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2178  ax-ext 2793
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2800  df-cleq 2814  df-clel 2892  df-nfc 2960  df-rab 3135  df-v 3473  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4267  df-if 4441  df-sn 4541  df-pr 4543  df-op 4547  df-br 5040  df-opab 5102  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-rn 5539  df-fun 6330  df-fn 6331  df-f 6332
This theorem is referenced by:  ftpg  6891  fpropnf1  6999  suppsnop  7819  seqomlem2  8062  addnqf  10347  mulnqf  10348  isumsup2  15180  ruclem6  15567  sadcf  15779  sadadd2lem  15785  sadadd3  15787  sadaddlem  15792  smupf  15804  algrf  15894  funcoppc  17124  pmtr3ncomlem1  18580  znf1o  20674  ovolfsf  24054  ovolsf  24055  ovoliunlem1  24085  ovoliun  24088  ovoliun2  24089  voliunlem3  24135  itgss3  24397  dvexp  24535  efcn  25017  gamf  25607  basellem9  25653  axlowdimlem10  26724  wlkres  27439  1wlkdlem1  27901  vsfval  28395  ho0f  29513  opsqrlem4  29905  pjinvari  29953  fmptdF  30388  omssubaddlem  31565  omssubadd  31566  sitgclg  31608  sitgaddlemb  31614  coinfliprv  31748  plymul02  31824  signshf  31866  circum  32925  knoppcnlem8  33847  knoppcnlem11  33850  poimirlem31  34970  diophren  39561  clsf2  40639  seff  40824  binomcxplemnotnn0  40871  volicoff  42456  fourierdlem62  42629  fourierdlem80  42647  fourierdlem97  42664  carageniuncllem2  42980  0ome  42987  fundcmpsurinjimaid  43747  mapprop  44566  lindslinindimp2lem2  44686  zlmodzxzldeplem1  44727  line2  44973
  Copyright terms: Public domain W3C validator