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  7034  en1  7090  en2  7116  xpen  7149  phplem4  7160  phplem4on  7173  dif1en  7187  fiintim  7242  residfi  7258  supisolem  7354  ordiso2  7381  inresflem  7406  eldju  7414  caseinl  7437  caseinr  7438  enomnilem  7484  enmkvlem  7507  enwomnilem  7515  iseqf1olemnab  10959  hashfacen  11306  hashf1lem1  11307  fprodssdc  12382  phimullem  13032  ballotfilemsima  13317  gsump1  14247  znleval  15097