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

Theorem feq1i 6708
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 6698 . 2 (𝐹 = 𝐺 → (𝐹:𝐴𝐵𝐺:𝐴𝐵))
31, 2ax-mp 5 1 (𝐹:𝐴𝐵𝐺:𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 205   = wceq 1540  wf 6539
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3432  df-v 3475  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149  df-opab 5211  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-fun 6545  df-fn 6546  df-f 6547
This theorem is referenced by:  ftpg  7156  fpropnf1  7269  suppsnop  8168  seqomlem2  8457  addnqf  10949  mulnqf  10950  isumsup2  15799  ruclem6  16185  sadcf  16401  sadadd2lem  16407  sadadd3  16409  sadaddlem  16414  smupf  16426  algrf  16517  funcoppc  17832  pmtr3ncomlem1  19386  znf1o  21330  ovolfsf  25233  ovolsf  25234  ovoliunlem1  25264  ovoliun  25267  ovoliun2  25268  voliunlem3  25314  itgss3  25577  dvexp  25718  efcn  26206  gamf  26798  basellem9  26844  axlowdimlem10  28491  wlkres  29209  1wlkdlem1  29672  vsfval  30168  ho0f  31286  opsqrlem4  31678  pjinvari  31726  fmptdF  32163  omssubaddlem  33611  omssubadd  33612  sitgclg  33654  sitgaddlemb  33660  coinfliprv  33794  plymul02  33870  signshf  33912  circum  34972  knoppcnlem8  35692  knoppcnlem11  35695  poimirlem31  36835  diophren  41866  clsf2  43192  seff  43383  binomcxplemnotnn0  43430  volicoff  45022  fourierdlem62  45195  fourierdlem80  45213  fourierdlem97  45230  carageniuncllem2  45549  0ome  45556  fcoresf1  46090  fcoresfo  46092  fundcmpsurinjimaid  46390  lindslinindimp2lem2  47240  zlmodzxzldeplem1  47281  line2  47538
  Copyright terms: Public domain W3C validator