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

Theorem f1ofun 5375
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 5374 . 2 (𝐹:𝐴1-1-onto𝐵𝐹 Fn 𝐴)
2 fnfun 5226 . 2 (𝐹 Fn 𝐴 → Fun 𝐹)
31, 2syl 14 1 (𝐹:𝐴1-1-onto𝐵 → Fun 𝐹)
Colors of variables: wff set class
Syntax hints:  wi 4  Fun wfun 5123   Fn wfn 5124  1-1-ontowf1o 5128
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 5132  df-f 5133  df-f1 5134  df-f1o 5136
This theorem is referenced by:  f1orel  5376  f1oresrab  5591  isose  5728  f1opw  5983  xpcomco  6726  fiintim  6823  f1dmvrnfibi  6838  caseinl  6982  caseinr  6983  ctssdccl  7002  ctssdclemr  7003  fihasheqf1oi  10564  fisumss  11191  ennnfonelemex  11956  ennnfonelemf1  11960  hmeontr  12514
  Copyright terms: Public domain W3C validator