Theorem f1ofn 5361

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 5360	. 2 |- ( F : A -1-1-onto-> B -> F : A --> B )
2		ffn 5267	. 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 5113   -->wf 5114   -1-1-onto->wf1o 5117

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 5122  df-f1 5123  df-f1o 5125

This theorem is referenced by:  f1ofun  5362  f1odm  5364  isocnv2  5706  isoini  5712  isoselem  5714  bren  6634  en1  6686  xpen  6732  phplem4  6742  phplem4on  6754  dif1en  6766  fiintim  6810  supisolem  6888  ordiso2  6913  inresflem  6938  eldju  6946  caseinl  6969  caseinr  6970  enomnilem  7003  iseqf1olemnab  10254  hashfacen  10572  phimullem  11890