Theorem f1fn 5485

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

Syntax hints:   -> wi 4   Fn wfn 5267   -->wf 5268   -1-1->wf1 5269

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 5276  df-f1 5277

This theorem is referenced by:  f1fun  5486  f1rel  5487  f1dm  5488  f1ssr  5490  f1f1orn  5535  f1elima  5844  f1eqcocnv  5862  f1oiso  5897  phplem4dom  6961  f1finf1o  7051  updjudhcoinlf  7184  updjudhcoinrg  7185  updjud  7186  fihashf1rn  10935  kerf1ghm  13643  domomsubct  15975