Theorem f1f 5531

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

Syntax hints:   -> wi 4   `'ccnv 4718   Fun wfun 5312   -->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-f1 5323

This theorem is referenced by:  f1rn  5532  f1fn  5533  f1ss  5537  f1ssres  5540  f1of  5572  dff1o5  5581  fsnd  5616  cocan1  5911  f1o2ndf1  6374  brdomg  6897  f1dom2g  6907  f1domg  6909  dom3d  6925  f1imaen2g  6945  2dom  6958  dom1o  6977  xpdom2  6990  dom0  6999  phplem4dom  7023  isinfinf  7059  infm  7066  updjudhcoinlf  7247  updjudhcoinrg  7248  casef1  7257  djudom  7260  difinfsnlem  7266  difinfsn  7267  seqf1oglem1  10741  fihashf1rn  11010  ennnfonelemrn  12990  reeff1o  15447  ushgruhgr  15880  umgr0e  15918  usgredgssen  15960  ausgrusgrben  15966  usgrss  15975  uspgrupgr  15979  usgrumgr  15982  usgrislfuspgrdom  15988  ushgredgedg  16024  ushgredgedgloop  16026  1dom1el  16354  pwle2  16364