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

Theorem f1ofun 5455
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 5454 . 2 (𝐹:𝐴1-1-onto𝐵𝐹 Fn 𝐴)
2 fnfun 5305 . 2 (𝐹 Fn 𝐴 → Fun 𝐹)
31, 2syl 14 1 (𝐹:𝐴1-1-onto𝐵 → Fun 𝐹)
Colors of variables: wff set class
Syntax hints:  wi 4  Fun wfun 5202   Fn wfn 5203  1-1-ontowf1o 5207
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 5211  df-f 5212  df-f1 5213  df-f1o 5215
This theorem is referenced by:  f1orel  5456  f1oresrab  5673  isose  5812  f1opw  6068  xpcomco  6816  fiintim  6918  f1dmvrnfibi  6933  caseinl  7080  caseinr  7081  ctssdccl  7100  ctssdclemr  7101  fihasheqf1oi  10734  fisumss  11367  ennnfonelemex  12381  ennnfonelemf1  12385  hmeontr  13306
  Copyright terms: Public domain W3C validator