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

Theorem f1ofn 5417
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 5416 . 2  |-  ( F : A -1-1-onto-> B  ->  F : A
--> B )
2 ffn 5321 . 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 5167   -->wf 5168   -1-1-onto->wf1o 5171
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-f 5176  df-f1 5177  df-f1o 5179
This theorem is referenced by:  f1ofun  5418  f1odm  5420  isocnv2  5764  isoini  5770  isoselem  5772  bren  6694  en1  6746  xpen  6792  phplem4  6802  phplem4on  6814  dif1en  6826  fiintim  6875  supisolem  6954  ordiso2  6981  inresflem  7006  eldju  7014  caseinl  7037  caseinr  7038  enomnilem  7083  enmkvlem  7106  enwomnilem  7114  iseqf1olemnab  10396  hashfacen  10718  fprodssdc  11498  phimullem  12115
  Copyright terms: Public domain W3C validator