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

Theorem f1ofn 5334
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 5333 . 2  |-  ( F : A -1-1-onto-> B  ->  F : A
--> B )
2 ffn 5240 . 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 5086   -->wf 5087   -1-1-onto->wf1o 5090
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 5095  df-f1 5096  df-f1o 5098
This theorem is referenced by:  f1ofun  5335  f1odm  5337  isocnv2  5679  isoini  5685  isoselem  5687  bren  6607  en1  6659  xpen  6705  phplem4  6715  phplem4on  6727  dif1en  6739  fiintim  6783  supisolem  6861  ordiso2  6886  inresflem  6911  eldju  6919  caseinl  6942  caseinr  6943  enomnilem  6976  iseqf1olemnab  10201  hashfacen  10519  phimullem  11796
  Copyright terms: Public domain W3C validator