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

Theorem f1f 5120
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 4935 . 2  |-  ( F : A -1-1-> B  <->  ( F : A --> B  /\  Fun  `' F ) )
21simplbi 263 1  |-  ( F : A -1-1-> B  ->  F : A --> B )
Colors of variables: wff set class
Syntax hints:    -> wi 4   `'ccnv 4372   Fun wfun 4924   -->wf 4926   -1-1->wf1 4927
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103
This theorem depends on definitions:  df-bi 114  df-f1 4935
This theorem is referenced by:  f1fn  5121  f1ss  5125  f1ssres  5127  f1of  5154  dff1o5  5163  fun11iun  5175  cocan1  5455  f1dmex  5771  f1o2ndf1  5877  brdomg  6260  f1dom2g  6267  f1domg  6269  dom3d  6285  f1imaen2g  6304  2dom  6316  xpdom2  6336  phplem4dom  6355
  Copyright terms: Public domain W3C validator