Theorem f1ofn 5254

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 5253	. 2 |- ( F : A -1-1-onto-> B -> F : A --> B )
2		ffn 5161	. 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 5010   -->wf 5011   -1-1-onto->wf1o 5014

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104

This theorem depends on definitions:  df-bi 115  df-f 5019  df-f1 5020  df-f1o 5022

This theorem is referenced by:  f1ofun  5255  f1odm  5257  isocnv2  5591  isoini  5597  isoselem  5599  bren  6462  en1  6514  xpen  6559  phplem4  6569  phplem4on  6581  dif1en  6593  fiintim  6637  supisolem  6701  ordiso2  6726  inresflem  6750  eldju  6757  enomnilem  6792  iseqf1olemnab  9913  hashfacen  10237  phimullem  11475