Theorem f1ofn 5593

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 5592	. 2 |- ( F : A -1-1-onto-> B -> F : A --> B )
2		ffn 5489	. 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 5328   -->wf 5329   -1-1-onto->wf1o 5332

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 5337  df-f1 5338  df-f1o 5340

This theorem is referenced by:  f1ofun  5594  f1odm  5596  isocnv2  5963  isoini  5969  isoselem  5971  bren  6960  en1  7016  en2  7041  xpen  7074  phplem4  7084  phplem4on  7097  dif1en  7111  fiintim  7166  residfi  7182  supisolem  7267  ordiso2  7294  inresflem  7319  eldju  7327  caseinl  7350  caseinr  7351  enomnilem  7397  enmkvlem  7420  enwomnilem  7428  iseqf1olemnab  10826  hashfacen  11163  fprodssdc  12231  phimullem  12877  znleval  14749  gfsump1  16815