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

Theorem feq2i 5706
Description: Equality inference for functions. (Contributed by NM, 5-Sep-2011.)
Hypothesis
Ref Expression
feq2i.1  |-  A  =  B
Assertion
Ref Expression
feq2i  |-  ( F : A --> C  <->  F : B
--> C )

Proof of Theorem feq2i
StepHypRef Expression
1 feq2i.1 . 2  |-  A  =  B
2 feq2 5696 . 2  |-  ( A  =  B  ->  ( F : A --> C  <->  F : B
--> C ) )
31, 2ax-mp 5 1  |-  ( F : A --> C  <->  F : B
--> C )
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-ext 2380
This theorem depends on definitions:  df-bi 185  df-an 369  df-cleq 2394  df-fn 5571  df-f 5572
This theorem is referenced by:  fresaun  5738  fmpt2x  6849  fmpt2  6850  tposf  6985  issmo  7051  axdc3lem4  8864  cardf  8956  smobeth  8992  1fv  11845  seqf2  12168  hashf  12457  iswrddm0  12615  wrd0OLD  12617  wrd2pr2op  12939  ntrivcvgtail  13859  vdwlem8  14713  0ram  14745  gsumws1  16329  ga0  16658  efgsp1  17077  efgsfo  17079  efgredleme  17083  efgred  17088  ablfaclem2  17455  islinds2  19138  pmatcollpw3fi1lem1  19577  0met  21159  dvef  22671  dvfsumrlim2  22723  dchrisum0  24084  trgcgrg  24285  axlowdimlem4  24652  uhgra0  24713  umgra0  24729  0wlk  24951  0trl  24952  wlkntrl  24968  0spth  24977  constr1trl  24994  constr2wlk  25004  constr2trl  25005  usgra2wlkspthlem2  25024  constr3trllem3  25056  constr3trllem4  25057  grposn  25617  padct  27978  mbfmcnt  28702  coinfliprv  28913  fdc  31500  rabren3dioph  35090  fourierdlem80  37318  nnsum4primesodd  37825  nnsum4primesoddALTV  37826  nnsum4primeseven  37829  nnsum4primesevenALTV  37830  2ffzoeq  37953  uhg0e  37986
  Copyright terms: Public domain W3C validator