Theorem f1ofn 5584

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 5583	. 2 |- ( F : A -1-1-onto-> B -> F : A --> B )
2		ffn 5482	. 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 5321   -->wf 5322   -1-1-onto->wf1o 5325

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 5330  df-f1 5331  df-f1o 5333

This theorem is referenced by:  f1ofun  5585  f1odm  5587  isocnv2  5952  isoini  5958  isoselem  5960  bren  6916  en1  6972  en2  6997  xpen  7030  phplem4  7040  phplem4on  7053  dif1en  7067  fiintim  7122  residfi  7138  supisolem  7206  ordiso2  7233  inresflem  7258  eldju  7266  caseinl  7289  caseinr  7290  enomnilem  7336  enmkvlem  7359  enwomnilem  7367  iseqf1olemnab  10762  hashfacen  11099  fprodssdc  12150  phimullem  12796  znleval  14666