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  10969  fihashf1rn  11241  hashf1lem1  11299  ennnfonelemrn  13359  reeff1o  15923  birthdaylem1g  16144  ushgruhgr  16419  umgr0e  16457  usgredgssen  16501  ausgrusgrben  16507  usgrss  16516  uspgrupgr  16520  usgrumgr  16523  usgrislfuspgrdom  16529  ushgredgedg  16565  ushgredgedgloop  16567  trlsegvdeglem6  16804  trlsegvdeglem7  16805  trlsegvdegfi  16806  eupth2lem3lem2fi  16808  eupth2lem3lem3fi  16809  eupth2lem3lem6fi  16810  eupth2lem3lem4fi  16812  3dom  17116  pwle2  17126