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

Theorem feq2i 5547
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 5538 . 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 1369   -->wf 5409
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-cleq 2431  df-fn 5416  df-f 5417
This theorem is referenced by:  fresaun  5577  fmpt2x  6635  fmpt2  6636  tposf  6768  issmo  6801  axdc3lem4  8614  cardf  8706  smobeth  8742  1fv  11524  seqf2  11817  hashf  12102  wrd0  12244  iswrddm0  12246  wrd2pr2op  12539  vdwlem8  14041  0ram  14073  gsumws1  15508  ga0  15807  efgsp1  16225  efgsfo  16227  efgredleme  16231  efgred  16236  ablfaclem2  16575  islinds2  18217  0met  19916  dvef  21427  dvfsumrlim2  21479  dchrisum0  22744  trgcgrg  22942  axlowdimlem4  23142  uhgra0  23194  umgra0  23210  0wlk  23395  0trl  23396  wlkntrl  23412  0spth  23421  constr1trl  23438  constr2wlk  23448  constr2trl  23449  constr3trllem3  23489  constr3trllem4  23490  grposn  23653  mbfmcnt  26635  coinfliprv  26817  ntrivcvgtail  27366  fdc  28594  rabren3dioph  29107  2ffzoeq  30167  usgra2wlkspthlem2  30250
  Copyright terms: Public domain W3C validator