Theorem f1f 5542

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 5331	. 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 4724   Fun wfun 5320   -->wf 5322   -1-1->wf1 5323

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 5331

This theorem is referenced by:  f1rn  5543  f1fn  5544  f1ss  5548  f1ssres  5551  f1of  5583  dff1o5  5592  fsnd  5628  cocan1  5928  f1o2ndf1  6393  brdomg  6919  f1dom2g  6929  f1domg  6931  dom3d  6947  f1imaen2g  6967  2dom  6980  1dom1el  6993  dom1o  7002  xpdom2  7015  dom0  7024  phplem4dom  7048  isinfinf  7086  infm  7096  updjudhcoinlf  7279  updjudhcoinrg  7280  casef1  7289  djudom  7292  difinfsnlem  7298  difinfsn  7299  seqf1oglem1  10782  fihashf1rn  11051  ennnfonelemrn  13058  reeff1o  15516  ushgruhgr  15950  umgr0e  15988  usgredgssen  16032  ausgrusgrben  16038  usgrss  16047  uspgrupgr  16051  usgrumgr  16054  usgrislfuspgrdom  16060  ushgredgedg  16096  ushgredgedgloop  16098  trlsegvdeglem6  16335  trlsegvdeglem7  16336  trlsegvdegfi  16337  eupth2lem3lem2fi  16339  eupth2lem3lem3fi  16340  eupth2lem3lem6fi  16341  eupth2lem3lem4fi  16343  3dom  16638  pwle2  16650