Theorem f1ofn 5463

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 5462	. 2 |- ( F : A -1-1-onto-> B -> F : A --> B )
2		ffn 5366	. 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 5212   -->wf 5213   -1-1-onto->wf1o 5216

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 5221  df-f1 5222  df-f1o 5224

This theorem is referenced by:  f1ofun  5464  f1odm  5466  isocnv2  5813  isoini  5819  isoselem  5821  bren  6747  en1  6799  xpen  6845  phplem4  6855  phplem4on  6867  dif1en  6879  fiintim  6928  supisolem  7007  ordiso2  7034  inresflem  7059  eldju  7067  caseinl  7090  caseinr  7091  enomnilem  7136  enmkvlem  7159  enwomnilem  7167  iseqf1olemnab  10488  hashfacen  10816  fprodssdc  11598  phimullem  12225