Theorem f1f 5323

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 5123	. 2 |- ( F : A -1-1-> B <-> ( F : A --> B /\ Fun `' F ) )
2	1	simplbi 272	1 |- ( F : A -1-1-> B -> F : A --> B )

Syntax hints:   -> wi 4   `'ccnv 4533   Fun wfun 5112   -->wf 5114   -1-1->wf1 5115

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

This theorem depends on definitions:  df-bi 116  df-f1 5123

This theorem is referenced by:  f1rn  5324  f1fn  5325  f1ss  5329  f1ssres  5332  f1of  5360  dff1o5  5369  fsnd  5403  cocan1  5681  f1o2ndf1  6118  brdomg  6635  f1dom2g  6643  f1domg  6645  dom3d  6661  f1imaen2g  6680  2dom  6692  xpdom2  6718  dom0  6725  phplem4dom  6749  isinfinf  6784  infm  6791  updjudhcoinlf  6958  updjudhcoinrg  6959  casef1  6968  djudom  6971  difinfsnlem  6977  difinfsn  6978  fihashf1rn  10528  ennnfonelemrn  11921  pwle2  13182