Theorem f1ofn 5464

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 5463	. 2 |- ( F : A -1-1-onto-> B -> F : A --> B )
2		ffn 5367	. 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 5213   -->wf 5214   -1-1-onto->wf1o 5217

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 5222  df-f1 5223  df-f1o 5225

This theorem is referenced by:  f1ofun  5465  f1odm  5467  isocnv2  5816  isoini  5822  isoselem  5824  bren  6750  en1  6802  xpen  6848  phplem4  6858  phplem4on  6870  dif1en  6882  fiintim  6931  supisolem  7010  ordiso2  7037  inresflem  7062  eldju  7070  caseinl  7093  caseinr  7094  enomnilem  7139  enmkvlem  7162  enwomnilem  7170  iseqf1olemnab  10491  hashfacen  10819  fprodssdc  11601  phimullem  12228