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

Step	Hyp	Ref	Expression
1		f1of 5416	. 2 |- ( F : A -1-1-onto-> B -> F : A --> B )
2		ffn 5321	. 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 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