Theorem f1ofn 5615

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

Step	Hyp	Ref	Expression
1		f1of 5614	. 2 |- ( F : A -1-1-onto-> B -> F : A --> B )
2		ffn 5508	. 2 |- ( F : A --> B -> F Fn A )
3	1, 2	syl 14	1 |- ( F : A -1-1-onto-> B -> F Fn A )

Syntax hints:   -> wi 4   Fn wfn 5347   -->wf 5348   -1-1-onto->wf1o 5351

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 5356  df-f1 5357  df-f1o 5359

This theorem is referenced by:  f1ofun  5616  f1odm  5618  isocnv2  5985  isoini  5991  isoselem  5993  bren  6983  en1  7039  en2  7065  xpen  7098  phplem4  7109  phplem4on  7122  dif1en  7136  fiintim  7191  residfi  7207  supisolem  7299  ordiso2  7326  inresflem  7351  eldju  7359  caseinl  7382  caseinr  7383  enomnilem  7429  enmkvlem  7452  enwomnilem  7460  iseqf1olemnab  10863  hashfacen  11208  fprodssdc  12276  phimullem  12922  znleval  14801  gfsump1  16868