Theorem f1fn 5483

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 5481	. 2 |- ( F : A -1-1-> B -> F : A --> B )
2		ffn 5425	. 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 5266   -->wf 5267   -1-1->wf1 5268

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

This theorem is referenced by:  f1fun  5484  f1rel  5485  f1dm  5486  f1ssr  5488  f1f1orn  5533  f1elima  5842  f1eqcocnv  5860  f1oiso  5895  phplem4dom  6959  f1finf1o  7049  updjudhcoinlf  7182  updjudhcoinrg  7183  updjud  7184  fihashf1rn  10933  kerf1ghm  13610  domomsubct  15938