Theorem f1f 5035

Description: A one-to-one mapping is a mapping. (Contributed by NM, 31-Dec-1996.)

Assertion

Ref	Expression
f1f	|- ( F :A -1-1->B -> F :A -->B)

Proof of Theorem f1f

Step	Hyp	Ref	Expression
1		df-f1 4850	. 2 |- ( F :A -1-1->B <-> ( F :A -->B /\ Fun `' F))
2	1	simplbi 259	1 |- ( F :A -1-1->B -> F :A -->B)

Syntax hints:   -> wi 4   `'ccnv 4287   Fun wfun 4839   -->wf 4841   -1-1->wf1 4842

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99

This theorem depends on definitions:  df-bi 110  df-f1 4850

This theorem is referenced by:  f1fn  5036  f1ss  5040  f1ssres  5042  f1of  5069  dff1o5  5078  fun11iun  5090  cocan1  5370  f1dmex  5685  f1o2ndf1  5791  brdomg  6165  f1dom2g  6172  f1domg  6174  dom3d  6190  f1imaen2g  6209  2dom  6221  xpdom2  6241