Theorem f1f 5336

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 5136	. 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 4546   Fun wfun 5125   -->wf 5127   -1-1->wf1 5128

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 5136

This theorem is referenced by:  f1rn  5337  f1fn  5338  f1ss  5342  f1ssres  5345  f1of  5375  dff1o5  5384  fsnd  5418  cocan1  5696  f1o2ndf1  6133  brdomg  6650  f1dom2g  6658  f1domg  6660  dom3d  6676  f1imaen2g  6695  2dom  6707  xpdom2  6733  dom0  6740  phplem4dom  6764  isinfinf  6799  infm  6806  updjudhcoinlf  6973  updjudhcoinrg  6974  casef1  6983  djudom  6986  difinfsnlem  6992  difinfsn  6993  fihashf1rn  10567  ennnfonelemrn  11968  reeff1o  12902  pwle2  13366