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

Theorem feq1i 5934
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 5924 . 2 (𝐹 = 𝐺 → (𝐹:𝐴𝐵𝐺:𝐴𝐵))
31, 2ax-mp 5 1 (𝐹:𝐴𝐵𝐺:𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 194   = wceq 1474  wf 5785
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
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 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-rab 2904  df-v 3174  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-br 4578  df-opab 4638  df-rel 5034  df-cnv 5035  df-co 5036  df-dm 5037  df-rn 5038  df-fun 5791  df-fn 5792  df-f 5793
This theorem is referenced by:  ftpg  6305  suppsnop  7173  seqomlem2  7410  addnqf  9626  mulnqf  9627  hashf  12943  isumsup2  14365  ruclem6  14751  sadcf  14961  sadadd2lem  14967  sadadd3  14969  sadaddlem  14974  smupf  14986  algrf  15072  funcoppc  16306  pmtr3ncomlem1  17664  znf1o  19666  ovolfsf  22991  ovolsf  22992  ovoliunlem1  23021  ovoliun  23024  ovoliun2  23025  voliunlem3  23071  itgss3  23331  dvexp  23466  efcn  23945  gamf  24513  basellem9  24559  axlowdimlem10  25576  uhgrares  25630  umgrares  25646  2trllemH  25875  2trllemG  25881  wlkntrllem1  25882  wlkntrllem3  25884  eupares  26295  vsfval  26665  ho0f  27787  opsqrlem4  28179  pjinvari  28227  fmptdF  28629  omssubaddlem  29481  omssubadd  29482  sitgclg  29524  sitgaddlemb  29530  coinfliprv  29664  plymul02  29742  signshf  29784  circum  30615  knoppcnlem8  31453  knoppcnlem11  31456  poimirlem31  32393  diophren  36178  clsf2  37227  seff  37313  binomcxplemnotnn0  37360  volicoff  38671  fourierdlem62  38844  fourierdlem80  38862  fourierdlem97  38879  carageniuncllem2  39195  0ome  39202  fpropnf1  40143  1wlkres  40860  11wlkdlem1  41285  mapprop  41898  lindslinindimp2lem2  42023  zlmodzxzldeplem1  42064
  Copyright terms: Public domain W3C validator