Theorem f1ofn 5573

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 5572	. 2 |- ( F : A -1-1-onto-> B -> F : A --> B )
2		ffn 5473	. 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 5313   -->wf 5314   -1-1-onto->wf1o 5317

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 5322  df-f1 5323  df-f1o 5325

This theorem is referenced by:  f1ofun  5574  f1odm  5576  isocnv2  5936  isoini  5942  isoselem  5944  bren  6895  en1  6951  en2  6973  xpen  7006  phplem4  7016  phplem4on  7029  dif1en  7041  fiintim  7093  residfi  7107  supisolem  7175  ordiso2  7202  inresflem  7227  eldju  7235  caseinl  7258  caseinr  7259  enomnilem  7305  enmkvlem  7328  enwomnilem  7336  iseqf1olemnab  10723  hashfacen  11058  fprodssdc  12101  phimullem  12747  znleval  14617