Theorem f1fn 5669

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 5668	. 2 |- ( F : A -1-1-> B -> F : A --> B )
2		ffn 5620	. 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 5478   -->wf 5479   -1-1->wf1 5480

This theorem is referenced by:  f1fun  5670  f1rel  5671  f1dm  5672  f1ssr  5674  f1f1orn  5714  f1elima  6038  f1eqcocnv  6057  domunsncan  7237  marypha2  7473  infdifsn  7640  acndom  7963  dfac12lem2  8055  ackbij1  8149  fin23lem32  8255  fin1a2lem5  8315  fin1a2lem6  8316  pwfseqlem1  8564  hashf1lem1  11735  hashf1  11737  odf1o2  15238  2ndcdisj  17550  qtopf1  17879  usgraedgrn  21432  kerf1hrm  24293  erdszelem10  24917  frlmlbs  27264  f1lindf  27307  usgfidegfi  28449  dihfn  32164  dihcl  32166  dih1dimatlem  32225  dochocss  32262

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

This theorem depends on definitions:  df-bi 179  df-an 362  df-f 5487  df-f1 5488