Theorem f1ofn 5643

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 5642	. 2 |- ( F : A -1-1-onto-> B -> F : A --> B )
2		ffn 5536	. 2 |- ( F : A --> B -> F Fn A )
3	1, 2	syl 14	1 |- ( F : A -1-1-onto-> B -> F Fn A )

This proof depends on syntax axioms:   -> wi 4   Fn wfn 5375   -->wf 5376   -1-1-onto->wf1o 5379

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117  df-f 5384  df-f1 5385  df-f1o 5387

This theorem is used by:  f1ofun  5644  f1odm  5646  isocnv2  6021  isoini  6027  isoselem  6029  bren  7036  en1  7092  en2  7118  xpen  7151  phplem4  7162  phplem4on  7175  dif1en  7189  fiintim  7244  residfi  7260  supisolem  7354  ordiso2  7381  inresflem  7406  eldju  7414  caseinl  7437  caseinr  7438  enomnilem  7484  enmkvlem  7507  enwomnilem  7515  iseqf1olemnab  10958  hashfacen  11305  hashf1lem1  11306  fprodssdc  12381  phimullem  13031  ballotfilemsima  13316  gsump1  14246  znleval  15096