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  7038  f1dom2g  7048  f1domg  7050  dom3d  7066  f1imaen2g  7086  2dom  7099  1dom1el  7113  dom1o  7122  xpdom2  7135  dom0  7144  phplem4dom  7169  isinfinf  7207  infm  7217  f1setfi  7322  updjudhcoinlf  7426  updjudhcoinrg  7427  casef1  7436  djudom  7439  difinfsnlem  7445  difinfsn  7446  seqf1oglem1  10976  fihashf1rn  11248  hashf1lem1  11306  ennnfonelemrn  13367  reeff1o  16016  birthdaylem1g  16242  ushgruhgr  16543  umgr0e  16581  usgredgssen  16625  ausgrusgrben  16631  usgrss  16640  uspgrupgr  16644  usgrumgr  16647  usgrislfuspgrdom  16653  ushgredgedg  16689  ushgredgedgloop  16691  trlsegvdeglem6  16928  trlsegvdeglem7  16929  trlsegvdegfi  16930  eupth2lem3lem2fi  16932  eupth2lem3lem3fi  16933  eupth2lem3lem6fi  16934  eupth2lem3lem4fi  16936  3dom  17240  pwle2  17250