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

Theorem f1ofun 5362
Description: A one-to-one onto mapping is a function. (Contributed by NM, 12-Dec-2003.)
Assertion
Ref Expression
f1ofun  |-  ( F : A -1-1-onto-> B  ->  Fun  F )

Proof of Theorem f1ofun
StepHypRef Expression
1 f1ofn 5361 . 2  |-  ( F : A -1-1-onto-> B  ->  F  Fn  A )
2 fnfun 5215 . 2  |-  ( F  Fn  A  ->  Fun  F )
31, 2syl 14 1  |-  ( F : A -1-1-onto-> B  ->  Fun  F )
Colors of variables: wff set class
Syntax hints:    -> wi 4   Fun wfun 5112    Fn wfn 5113   -1-1-onto->wf1o 5117
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-fn 5121  df-f 5122  df-f1 5123  df-f1o 5125
This theorem is referenced by:  f1orel  5363  f1oresrab  5578  isose  5715  f1opw  5970  xpcomco  6713  fiintim  6810  f1dmvrnfibi  6825  caseinl  6969  caseinr  6970  ctssdccl  6989  ctssdclemr  6990  fihasheqf1oi  10527  fisumss  11154  ennnfonelemex  11916  ennnfonelemf1  11920  hmeontr  12471
  Copyright terms: Public domain W3C validator