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

Theorem f1ofun 5463
Description: A one-to-one onto mapping is a function. (Contributed by NM, 12-Dec-2003.)
Assertion
Ref Expression
f1ofun (𝐹:𝐴1-1-onto𝐵 → Fun 𝐹)

Proof of Theorem f1ofun
StepHypRef Expression
1 f1ofn 5462 . 2 (𝐹:𝐴1-1-onto𝐵𝐹 Fn 𝐴)
2 fnfun 5313 . 2 (𝐹 Fn 𝐴 → Fun 𝐹)
31, 2syl 14 1 (𝐹:𝐴1-1-onto𝐵 → Fun 𝐹)
Colors of variables: wff set class
Syntax hints:  wi 4  Fun wfun 5210   Fn wfn 5211  1-1-ontowf1o 5215
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106
This theorem depends on definitions:  df-bi 117  df-fn 5219  df-f 5220  df-f1 5221  df-f1o 5223
This theorem is referenced by:  f1orel  5464  f1oresrab  5681  isose  5821  f1opw  6077  xpcomco  6825  fiintim  6927  f1dmvrnfibi  6942  caseinl  7089  caseinr  7090  ctssdccl  7109  ctssdclemr  7110  fihasheqf1oi  10766  fisumss  11399  ennnfonelemex  12414  ennnfonelemf1  12418  hmeontr  13783
  Copyright terms: Public domain W3C validator