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  7421  updjudhcoinrg  7422  casef1  7431  djudom  7434  difinfsnlem  7440  difinfsn  7441  seqf1oglem1  10971  fihashf1rn  11243  hashf1lem1  11301  ennnfonelemrn  13362  reeff1o  15965  birthdaylem1g  16186  ushgruhgr  16487  umgr0e  16525  usgredgssen  16569  ausgrusgrben  16575  usgrss  16584  uspgrupgr  16588  usgrumgr  16591  usgrislfuspgrdom  16597  ushgredgedg  16633  ushgredgedgloop  16635  trlsegvdeglem6  16872  trlsegvdeglem7  16873  trlsegvdegfi  16874  eupth2lem3lem2fi  16876  eupth2lem3lem3fi  16877  eupth2lem3lem6fi  16878  eupth2lem3lem4fi  16880  3dom  17184  pwle2  17194