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

Theorem feq1i 5705
Description: Equality inference for functions. (Contributed by Paul Chapman, 22-Jun-2011.)
Hypothesis
Ref Expression
feq1i.1  |-  F  =  G
Assertion
Ref Expression
feq1i  |-  ( F : A --> B  <->  G : A
--> B )

Proof of Theorem feq1i
StepHypRef Expression
1 feq1i.1 . 2  |-  F  =  G
2 feq1 5695 . 2  |-  ( F  =  G  ->  ( F : A --> B  <->  G : A
--> B ) )
31, 2ax-mp 5 1  |-  ( F : A --> B  <->  G : A
--> B )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    = wceq 1405   -->wf 5564
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-rab 2762  df-v 3060  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-nul 3738  df-if 3885  df-sn 3972  df-pr 3974  df-op 3978  df-br 4395  df-opab 4453  df-rel 4829  df-cnv 4830  df-co 4831  df-dm 4832  df-rn 4833  df-fun 5570  df-fn 5571  df-f 5572
This theorem is referenced by:  ftpg  6060  suppsnop  6915  seqomlem2  7152  addnqf  9355  mulnqf  9356  hashf  12457  isumsup2  13807  ruclem6  14175  sadcf  14310  sadadd2lem  14316  sadadd3  14318  sadaddlem  14323  smupf  14335  algrf  14409  funcoppc  15486  pmtr3ncomlem1  16820  znf1o  18886  ovolfsf  22173  ovolsf  22174  ovoliunlem1  22203  ovoliun  22206  ovoliun2  22207  voliunlem3  22252  itgss3  22511  dvexp  22646  efcn  23128  gamf  23696  basellem9  23741  axlowdimlem10  24658  uhgrares  24712  umgrares  24728  2trllemH  24958  2trllemG  24964  wlkntrllem1  24965  wlkntrllem3  24967  eupares  25379  issubgoi  25712  vsfval  25928  ho0f  27069  opsqrlem4  27461  pjinvari  27509  fmptdF  27923  omssubaddlem  28733  omssubadd  28734  sitgclg  28776  coinfliprv  28913  plymul02  28995  signshf  29037  circum  29879  diophren  35088  seff  36017  binomcxplemnotnn0  36089  fourierdlem62  37300  fourierdlem80  37318  fourierdlem97  37335  uhgres  37989  mapprop  38427  lindslinindimp2lem2  38552  zlmodzxzldeplem1  38593
  Copyright terms: Public domain W3C validator