Theorem f1ofn 5635

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 5634	. 2 |- ( F : A -1-1-onto-> B -> F : A --> B )
2		ffn 5528	. 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 5367   -->wf 5368   -1-1-onto->wf1o 5371

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 5376  df-f1 5377  df-f1o 5379

This theorem is referenced by:  f1ofun  5636  f1odm  5638  isocnv2  6008  isoini  6014  isoselem  6016  bren  7020  en1  7076  en2  7102  xpen  7135  phplem4  7146  phplem4on  7159  dif1en  7173  fiintim  7228  residfi  7244  supisolem  7338  ordiso2  7365  inresflem  7390  eldju  7398  caseinl  7421  caseinr  7422  enomnilem  7468  enmkvlem  7491  enwomnilem  7499  iseqf1olemnab  10916  hashfacen  11262  hashf1lem1  11263  fprodssdc  12335  phimullem  12981  ballotfilemsima  13237  gsump1  14134  znleval  14960