Theorem f1fn 5438

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 5437	. 2 |- ( F : A -1-1-> B -> F : A --> B )
2		ffn 5389	. 2 |- ( F : A --> B -> F Fn A )
3	1, 2	syl 15	1 |- ( F : A -1-1-> B -> F Fn A )

Syntax hints:   -> wi 4   Fn wfn 5250   -->wf 5251   -1-1->wf1 5252

This theorem is referenced by:  f1fun  5439  f1rel  5440  f1dm  5441  f1ssr  5443  f1f1orn  5483  f1elima  5787  f1eqcocnv  5805  domunsncan  6962  marypha2  7192  infdifsn  7357  acndom  7678  dfac12lem2  7770  ackbij1  7864  fin23lem32  7970  fin1a2lem5  8030  fin1a2lem6  8031  pwfseqlem1  8280  hashf1lem1  11393  hashf1  11395  odf1o2  14884  2ndcdisj  17182  qtopf1  17507  erdszelem10  23731  frlmlbs  27249  f1lindf  27292  usgraedgrn  28125  dihfn  31458  dihcl  31460  dih1dimatlem  31519  dochocss  31556

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 177  df-an 360  df-f 5259  df-f1 5260