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 5601	. 2 |- ( F : A -1-1-> B -> F : A --> B )
2		ffn 5536	. 2 |- ( F : A --> B -> F Fn A )
3	1, 2	syl 14	1 |- ( F : A -1-1-> B -> F Fn A )

This proof depends on syntax axioms:   -> wi 4   Fn wfn 5375   -->wf 5376   -1-1->wf1 5377

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117  df-f 5384  df-f1 5385

This theorem is used by:  f1fun  5604  f1rel  5605  f1dm  5606  f1ssr  5608  f1f1orn  5653  f1elima  5982  f1eqcocnv  6000  f1oiso  6035  phplem4dom  7167  f1finf1o  7269  updjudhcoinlf  7426  updjudhcoinrg  7427  updjud  7428  fihashf1rn  11249  hashf1lem1  11307  hashf1  11309  kerf1ghm  14136  domomsubct  17236