Theorem f1fn 5505

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 5503	. 2 |- ( F : A -1-1-> B -> F : A --> B )
2		ffn 5445	. 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 5285   -->wf 5286   -1-1->wf1 5287

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 5294  df-f1 5295

This theorem is referenced by:  f1fun  5506  f1rel  5507  f1dm  5508  f1ssr  5510  f1f1orn  5555  f1elima  5865  f1eqcocnv  5883  f1oiso  5918  phplem4dom  6984  f1finf1o  7075  updjudhcoinlf  7208  updjudhcoinrg  7209  updjud  7210  fihashf1rn  10970  kerf1ghm  13725  domomsubct  16140