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

Theorem feq2i 5490
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 5481 . 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 176    = wceq 1647   -->wf 5354
This theorem is referenced by:  fresaun  5518  fmpt2x  6317  fmpt2  6318  tposf  6404  issmo  6507  axdc3lem4  8226  cardf  8319  smobeth  8355  1fv  11010  seqf2  11229  hashf  11512  wrd0  11619  s1cl  11642  vdwlem8  13243  0ram  13275  gsumws1  14672  ga0  14962  efgsp1  15256  efgsfo  15258  efgredleme  15262  efgred  15267  ablfaclem2  15531  0met  18143  dvef  19542  dvfsumrlim2  19594  dchrisum0  20892  uhgra0  21022  umgra0  21038  grposn  21193  mbfmcnt  24081  coinfliprv  24188  ntrivcvgtail  24712  axlowdimlem4  25315  fdc  25962  rabren3dioph  26404  islinds2  26789  0wlk  27699  0trl  27700  0spth  27715  constr1trl  27726  constr3trllem3  27778  constr3trllem4  27779
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-11 1751  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1547  df-cleq 2359  df-fn 5361  df-f 5362
  Copyright terms: Public domain W3C validator