Theorem f1f 5593

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

Syntax hints:   -> wi 4   `'ccnv 4768   Fun wfun 5366   -->wf 5368   -1-1->wf1 5369

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This theorem depends on definitions:  df-bi 117  df-f1 5377

This theorem is referenced by:  f1rn  5594  f1fn  5595  f1ss  5599  f1ssres  5602  f1of  5634  dff1o5  5643  fsnd  5679  cocan1  5983  f1o2ndf1  6454  brdomg  7022  f1dom2g  7032  f1domg  7034  dom3d  7050  f1imaen2g  7070  2dom  7083  1dom1el  7097  dom1o  7106  xpdom2  7119  dom0  7128  phplem4dom  7153  isinfinf  7191  infm  7201  f1setfi  7307  updjudhcoinlf  7410  updjudhcoinrg  7411  casef1  7420  djudom  7423  difinfsnlem  7429  difinfsn  7430  seqf1oglem1  10934  fihashf1rn  11205  hashf1lem1  11263  ennnfonelemrn  13288  reeff1o  15797  ushgruhgr  16235  umgr0e  16273  usgredgssen  16317  ausgrusgrben  16323  usgrss  16332  uspgrupgr  16336  usgrumgr  16339  usgrislfuspgrdom  16345  ushgredgedg  16381  ushgredgedgloop  16383  trlsegvdeglem6  16620  trlsegvdeglem7  16621  trlsegvdegfi  16622  eupth2lem3lem2fi  16624  eupth2lem3lem3fi  16625  eupth2lem3lem6fi  16626  eupth2lem3lem4fi  16628  3dom  16932  pwle2  16942