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

Theorem feq1i 5714
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 5704 . 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 1374   -->wf 5575
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-rab 2816  df-v 3108  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-sn 4021  df-pr 4023  df-op 4027  df-br 4441  df-opab 4499  df-rel 4999  df-cnv 5000  df-co 5001  df-dm 5002  df-rn 5003  df-fun 5581  df-fn 5582  df-f 5583
This theorem is referenced by:  ftpg  6062  suppsnop  6905  seqomlem2  7106  addnqf  9315  mulnqf  9316  hashf  12367  isumsup2  13610  ruclem6  13818  sadcf  13951  sadadd2lem  13957  sadadd3  13959  sadaddlem  13964  smupf  13976  algrf  14050  funcoppc  15091  pmtr3ncomlem1  16287  znf1o  18350  ovolfsf  21611  ovolsf  21612  ovoliunlem1  21641  ovoliun  21644  ovoliun2  21645  voliunlem3  21690  itgss3  21949  dvexp  22084  efcn  22565  basellem9  23083  axlowdimlem10  23923  uhgrares  23971  umgrares  23987  2trllemH  24216  2trllemG  24222  wlkntrllem1  24223  wlkntrllem3  24225  eupares  24637  issubgoi  24974  vsfval  25190  ho0f  26332  opsqrlem4  26724  pjinvari  26772  fmptdF  27153  sitgclg  27910  coinfliprv  28047  plymul02  28129  signshf  28171  gamf  28211  circum  28501  diophren  30338  seff  30781  fourierdlem62  31424  fourierdlem97  31459  mapprop  31874  lindslinindimp2lem2  32008  zlmodzxzldeplem1  32057
  Copyright terms: Public domain W3C validator