Theorem f1fn 5547

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 5545	. 2 |- ( F : A -1-1-> B -> F : A --> B )
2		ffn 5484	. 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 5323   -->wf 5324   -1-1->wf1 5325

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 5332  df-f1 5333

This theorem is referenced by:  f1fun  5548  f1rel  5549  f1dm  5550  f1ssr  5552  f1f1orn  5597  f1elima  5919  f1eqcocnv  5937  f1oiso  5972  phplem4dom  7053  f1finf1o  7151  updjudhcoinlf  7284  updjudhcoinrg  7285  updjud  7286  fihashf1rn  11056  kerf1ghm  13884  domomsubct  16662