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

Theorem f1f 5210
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 5015 . 2  |-  ( F : A -1-1-> B  <->  ( F : A --> B  /\  Fun  `' F ) )
21simplbi 268 1  |-  ( F : A -1-1-> B  ->  F : A --> B )
Colors of variables: wff set class
Syntax hints:    -> wi 4   `'ccnv 4435   Fun wfun 5004   -->wf 5006   -1-1->wf1 5007
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104
This theorem depends on definitions:  df-bi 115  df-f1 5015
This theorem is referenced by:  f1rn  5211  f1fn  5212  f1ss  5216  f1ssres  5219  f1of  5247  dff1o5  5256  cocan1  5558  f1o2ndf1  5985  brdomg  6455  f1dom2g  6463  f1domg  6465  dom3d  6481  f1imaen2g  6500  2dom  6512  xpdom2  6537  dom0  6544  phplem4dom  6568  isinfinf  6603  infm  6610  updjudhcoinlf  6761  updjudhcoinrg  6762  casef1  6771  djudom  6777  fihashf1rn  10185
  Copyright terms: Public domain W3C validator