Theorem f1ofn 5523

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 5522	. 2 |- ( F : A -1-1-onto-> B -> F : A --> B )
2		ffn 5425	. 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 5266   -->wf 5267   -1-1-onto->wf1o 5270

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 5275  df-f1 5276  df-f1o 5278

This theorem is referenced by:  f1ofun  5524  f1odm  5526  isocnv2  5881  isoini  5887  isoselem  5889  bren  6835  en1  6891  en2  6912  xpen  6942  phplem4  6952  phplem4on  6964  dif1en  6976  fiintim  7028  residfi  7042  supisolem  7110  ordiso2  7137  inresflem  7162  eldju  7170  caseinl  7193  caseinr  7194  enomnilem  7240  enmkvlem  7263  enwomnilem  7271  iseqf1olemnab  10646  hashfacen  10981  fprodssdc  11901  phimullem  12547  znleval  14415