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

Theorem f1ofn 5462
Description: A one-to-one onto mapping is function on its domain. (Contributed by NM, 12-Dec-2003.)
Assertion
Ref Expression
f1ofn  |-  ( F : A -1-1-onto-> B  ->  F  Fn  A )

Proof of Theorem f1ofn
StepHypRef Expression
1 f1of 5461 . 2  |-  ( F : A -1-1-onto-> B  ->  F : A
--> B )
2 ffn 5365 . 2  |-  ( F : A --> B  ->  F  Fn  A )
31, 2syl 14 1  |-  ( F : A -1-1-onto-> B  ->  F  Fn  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    Fn wfn 5211   -->wf 5212   -1-1-onto->wf1o 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-f 5220  df-f1 5221  df-f1o 5223
This theorem is referenced by:  f1ofun  5463  f1odm  5465  isocnv2  5812  isoini  5818  isoselem  5820  bren  6746  en1  6798  xpen  6844  phplem4  6854  phplem4on  6866  dif1en  6878  fiintim  6927  supisolem  7006  ordiso2  7033  inresflem  7058  eldju  7066  caseinl  7089  caseinr  7090  enomnilem  7135  enmkvlem  7158  enwomnilem  7166  iseqf1olemnab  10487  hashfacen  10815  fprodssdc  11597  phimullem  12224
  Copyright terms: Public domain W3C validator