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

Theorem feq2i 5549
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 5540 . 2  |-  ( A  =  B  ->  ( F : A --> C  <->  F : B
--> C ) )
31, 2ax-mp 8 1  |-  ( F : A --> C  <->  F : B
--> C )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    = wceq 1649   -->wf 5413
This theorem is referenced by:  fresaun  5577  fmpt2x  6380  fmpt2  6381  tposf  6470  issmo  6573  axdc3lem4  8293  cardf  8385  smobeth  8421  1fv  11079  seqf2  11301  hashf  11584  wrd0  11691  s1cl  11714  vdwlem8  13315  0ram  13347  gsumws1  14744  ga0  15034  efgsp1  15328  efgsfo  15330  efgredleme  15334  efgred  15339  ablfaclem2  15603  0met  18353  dvef  19821  dvfsumrlim2  19873  dchrisum0  21171  uhgra0  21301  umgra0  21317  0wlk  21502  0trl  21503  wlkntrl  21519  0spth  21528  constr1trl  21545  constr2wlk  21555  constr2trl  21556  constr3trllem3  21596  constr3trllem4  21597  grposn  21760  mbfmcnt  24575  coinfliprv  24697  ntrivcvgtail  25185  axlowdimlem4  25792  fdc  26343  rabren3dioph  26770  islinds2  27155  iswrd0i  28003  usgra2wlkspthlem2  28041
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757  ax-ext 2389
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-cleq 2401  df-fn 5420  df-f 5421
  Copyright terms: Public domain W3C validator