Theorem f1f 5598

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 5382	. 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 4773   Fun wfun 5371   -->wf 5373   -1-1->wf1 5374

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 5382

This theorem is used by:  f1rn  5599  f1fn  5600  f1ss  5604  f1ssres  5607  f1of  5639  dff1o5  5648  fsnd  5684  cocan1  5993  f1o2ndf1  6464  brdomg  7032  f1dom2g  7042  f1domg  7044  dom3d  7060  f1imaen2g  7080  2dom  7093  1dom1el  7107  dom1o  7116  xpdom2  7129  dom0  7138  phplem4dom  7163  isinfinf  7201  infm  7211  f1setfi  7317  updjudhcoinlf  7420  updjudhcoinrg  7421  casef1  7430  djudom  7433  difinfsnlem  7439  difinfsn  7440  seqf1oglem1  10956  fihashf1rn  11227  hashf1lem1  11285  ennnfonelemrn  13310  reeff1o  15874  birthdaylem1g  16087  ushgruhgr  16321  umgr0e  16359  usgredgssen  16403  ausgrusgrben  16409  usgrss  16418  uspgrupgr  16422  usgrumgr  16425  usgrislfuspgrdom  16431  ushgredgedg  16467  ushgredgedgloop  16469  trlsegvdeglem6  16706  trlsegvdeglem7  16707  trlsegvdegfi  16708  eupth2lem3lem2fi  16710  eupth2lem3lem3fi  16711  eupth2lem3lem6fi  16712  eupth2lem3lem4fi  16714  3dom  17018  pwle2  17028