Theorem f1ofn 5443

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 5442	. 2 |- ( F : A -1-1-onto-> B -> F : A --> B )
2		ffn 5347	. 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 5193   -->wf 5194   -1-1-onto->wf1o 5197

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 5202  df-f1 5203  df-f1o 5205

This theorem is referenced by:  f1ofun  5444  f1odm  5446  isocnv2  5791  isoini  5797  isoselem  5799  bren  6725  en1  6777  xpen  6823  phplem4  6833  phplem4on  6845  dif1en  6857  fiintim  6906  supisolem  6985  ordiso2  7012  inresflem  7037  eldju  7045  caseinl  7068  caseinr  7069  enomnilem  7114  enmkvlem  7137  enwomnilem  7145  iseqf1olemnab  10444  hashfacen  10771  fprodssdc  11553  phimullem  12179