Theorem f1ofn 5545

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 5544	. 2 |- ( F : A -1-1-onto-> B -> F : A --> B )
2		ffn 5445	. 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 5285   -->wf 5286   -1-1-onto->wf1o 5289

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 5294  df-f1 5295  df-f1o 5297

This theorem is referenced by:  f1ofun  5546  f1odm  5548  isocnv2  5904  isoini  5910  isoselem  5912  bren  6858  en1  6914  en2  6936  xpen  6967  phplem4  6977  phplem4on  6990  dif1en  7002  fiintim  7054  residfi  7068  supisolem  7136  ordiso2  7163  inresflem  7188  eldju  7196  caseinl  7219  caseinr  7220  enomnilem  7266  enmkvlem  7289  enwomnilem  7297  iseqf1olemnab  10683  hashfacen  11018  fprodssdc  12016  phimullem  12662  znleval  14530