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

Theorem feq1i 6174
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 6164 . 2 (𝐹 = 𝐺 → (𝐹:𝐴𝐵𝐺:𝐴𝐵))
31, 2ax-mp 5 1 (𝐹:𝐴𝐵𝐺:𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 196   = wceq 1631  wf 6025
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-rab 3070  df-v 3353  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-sn 4317  df-pr 4319  df-op 4323  df-br 4787  df-opab 4847  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-fun 6031  df-fn 6032  df-f 6033
This theorem is referenced by:  ftpg  6565  fpropnf1  6666  suppsnop  7460  seqomlem2  7699  addnqf  9972  mulnqf  9973  hashfOLD  13326  isumsup2  14781  ruclem6  15166  sadcf  15379  sadadd2lem  15385  sadadd3  15387  sadaddlem  15392  smupf  15404  algrf  15490  funcoppc  16738  pmtr3ncomlem1  18096  znf1o  20111  ovolfsf  23455  ovolsf  23456  ovoliunlem1  23486  ovoliun  23489  ovoliun2  23490  voliunlem3  23536  itgss3  23797  dvexp  23932  efcn  24413  gamf  24986  basellem9  25032  axlowdimlem10  26048  wlkres  26798  1wlkdlem1  27313  vsfval  27824  ho0f  28946  opsqrlem4  29338  pjinvari  29386  fmptdF  29792  omssubaddlem  30697  omssubadd  30698  sitgclg  30740  sitgaddlemb  30746  coinfliprv  30880  plymul02  30959  signshf  31001  circum  31902  knoppcnlem8  32823  knoppcnlem11  32826  poimirlem31  33769  diophren  37900  clsf2  38947  seff  39031  binomcxplemnotnn0  39078  volicoff  40726  fourierdlem62  40899  fourierdlem80  40917  fourierdlem97  40934  carageniuncllem2  41253  0ome  41260  mapprop  42649  lindslinindimp2lem2  42773  zlmodzxzldeplem1  42814
  Copyright terms: Public domain W3C validator