Theorem f1fn 5533

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 5531	. 2 |- ( F : A -1-1-> B -> F : A --> B )
2		ffn 5473	. 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 5313   -->wf 5314   -1-1->wf1 5315

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 5322  df-f1 5323

This theorem is referenced by:  f1fun  5534  f1rel  5535  f1dm  5536  f1ssr  5538  f1f1orn  5583  f1elima  5897  f1eqcocnv  5915  f1oiso  5950  phplem4dom  7023  f1finf1o  7114  updjudhcoinlf  7247  updjudhcoinrg  7248  updjud  7249  fihashf1rn  11010  kerf1ghm  13811  domomsubct  16367