ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  f1f Unicode version

Theorem f1f 5298
Description: A one-to-one mapping is a mapping. (Contributed by NM, 31-Dec-1996.)
Assertion
Ref Expression
f1f  |-  ( F : A -1-1-> B  ->  F : A --> B )

Proof of Theorem f1f
StepHypRef Expression
1 df-f1 5098 . 2  |-  ( F : A -1-1-> B  <->  ( F : A --> B  /\  Fun  `' F ) )
21simplbi 272 1  |-  ( F : A -1-1-> B  ->  F : A --> B )
Colors of variables: wff set class
Syntax hints:    -> wi 4   `'ccnv 4508   Fun wfun 5087   -->wf 5089   -1-1->wf1 5090
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105
This theorem depends on definitions:  df-bi 116  df-f1 5098
This theorem is referenced by:  f1rn  5299  f1fn  5300  f1ss  5304  f1ssres  5307  f1of  5335  dff1o5  5344  fsnd  5378  cocan1  5656  f1o2ndf1  6093  brdomg  6610  f1dom2g  6618  f1domg  6620  dom3d  6636  f1imaen2g  6655  2dom  6667  xpdom2  6693  dom0  6700  phplem4dom  6724  isinfinf  6759  infm  6766  updjudhcoinlf  6933  updjudhcoinrg  6934  casef1  6943  djudom  6946  difinfsnlem  6952  difinfsn  6953  fihashf1rn  10503  ennnfonelemrn  11859  pwle2  13120
  Copyright terms: Public domain W3C validator