Theorem f1fn 5603

Description: A one-to-one mapping is a function on its domain. (Contributed by NM, 8-Mar-2014.)

Assertion

Ref	Expression
f1fn	|- ( F : A -1-1-> B -> F Fn A )

Proof of Theorem f1fn

Step	Hyp	Ref	Expression
1		f1f 5602	. 2 |- ( F : A -1-1-> B -> F : A --> B )
2		ffn 5554	. 2 |- ( F : A --> B -> F Fn A )
3	1, 2	syl 16	1 |- ( F : A -1-1-> B -> F Fn A )

Syntax hints:   -> wi 4   Fn wfn 5412   -->wf 5413   -1-1->wf1 5414

This theorem is referenced by:  f1fun  5604  f1rel  5605  f1dm  5606  f1ssr  5608  f1f1orn  5648  f1elima  5972  f1eqcocnv  5991  domunsncan  7171  marypha2  7406  infdifsn  7571  acndom  7892  dfac12lem2  7984  ackbij1  8078  fin23lem32  8184  fin1a2lem5  8244  fin1a2lem6  8245  pwfseqlem1  8493  hashf1lem1  11663  hashf1  11665  odf1o2  15166  2ndcdisj  17476  qtopf1  17805  usgraedgrn  21358  kerf1hrm  24219  erdszelem10  24843  frlmlbs  27121  f1lindf  27164  usgfidegfi  28094  dihfn  31755  dihcl  31757  dih1dimatlem  31816  dochocss  31853

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 178  df-an 361  df-f 5421  df-f1 5422