Theorem f1ofn 5505

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 5504	. 2 |- ( F : A -1-1-onto-> B -> F : A --> B )
2		ffn 5407	. 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 5253   -->wf 5254   -1-1-onto->wf1o 5257

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 5262  df-f1 5263  df-f1o 5265

This theorem is referenced by:  f1ofun  5506  f1odm  5508  isocnv2  5859  isoini  5865  isoselem  5867  bren  6806  en1  6858  xpen  6906  phplem4  6916  phplem4on  6928  dif1en  6940  fiintim  6992  residfi  7006  supisolem  7074  ordiso2  7101  inresflem  7126  eldju  7134  caseinl  7157  caseinr  7158  enomnilem  7204  enmkvlem  7227  enwomnilem  7235  iseqf1olemnab  10593  hashfacen  10928  fprodssdc  11755  phimullem  12393  znleval  14209