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  5927  f1o2ndf1  6392  brdomg  6918  f1dom2g  6928  f1domg  6930  dom3d  6946  f1imaen2g  6966  2dom  6979  1dom1el  6992  dom1o  7001  xpdom2  7014  dom0  7023  phplem4dom  7047  isinfinf  7085  infm  7095  updjudhcoinlf  7278  updjudhcoinrg  7279  casef1  7288  djudom  7291  difinfsnlem  7297  difinfsn  7298  seqf1oglem1  10780  fihashf1rn  11049  ennnfonelemrn  13039  reeff1o  15496  ushgruhgr  15930  umgr0e  15968  usgredgssen  16012  ausgrusgrben  16018  usgrss  16027  uspgrupgr  16031  usgrumgr  16034  usgrislfuspgrdom  16040  ushgredgedg  16076  ushgredgedgloop  16078  trlsegvdeglem6  16315  trlsegvdeglem7  16316  3dom  16587  pwle2  16599