Theorem f1f 5601

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

This proof depends on syntax axioms:   -> wi 4   `'ccnv 4775   Fun wfun 5374   -->wf 5376   -1-1->wf1 5377

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117  df-f1 5385

This theorem is used by:  f1rn  5602  f1fn  5603  f1ss  5607  f1ssres  5610  f1of  5642  dff1o5  5651  fsnd  5687  cocan1  5996  f1o2ndf1  6468  brdomg  7036  f1dom2g  7046  f1domg  7048  dom3d  7064  f1imaen2g  7084  2dom  7097  1dom1el  7111  dom1o  7120  xpdom2  7133  dom0  7142  phplem4dom  7167  isinfinf  7205  infm  7215  f1setfi  7322  updjudhcoinlf  7426  updjudhcoinrg  7427  casef1  7436  djudom  7439  difinfsnlem  7445  difinfsn  7446  seqf1oglem1  10977  fihashf1rn  11249  hashf1lem1  11307  ennnfonelemrn  13368  reeff1o  15999  birthdaylem1g  16225  ushgruhgr  16526  umgr0e  16564  usgredgssen  16608  ausgrusgrben  16614  usgrss  16623  uspgrupgr  16627  usgrumgr  16630  usgrislfuspgrdom  16636  ushgredgedg  16672  ushgredgedgloop  16674  trlsegvdeglem6  16911  trlsegvdeglem7  16912  trlsegvdegfi  16913  eupth2lem3lem2fi  16915  eupth2lem3lem3fi  16916  eupth2lem3lem6fi  16917  eupth2lem3lem4fi  16919  3dom  17223  pwle2  17233