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

Theorem f1f 5328
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 5128 . 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 4538   Fun wfun 5117   -->wf 5119   -1-1->wf1 5120
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 5128
This theorem is referenced by:  f1rn  5329  f1fn  5330  f1ss  5334  f1ssres  5337  f1of  5367  dff1o5  5376  fsnd  5410  cocan1  5688  f1o2ndf1  6125  brdomg  6642  f1dom2g  6650  f1domg  6652  dom3d  6668  f1imaen2g  6687  2dom  6699  xpdom2  6725  dom0  6732  phplem4dom  6756  isinfinf  6791  infm  6798  updjudhcoinlf  6965  updjudhcoinrg  6966  casef1  6975  djudom  6978  difinfsnlem  6984  difinfsn  6985  fihashf1rn  10547  ennnfonelemrn  11943  reeff1o  12877  pwle2  13277
  Copyright terms: Public domain W3C validator