Theorem f1f 5539

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 5329	. 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 4722   Fun wfun 5318   -->wf 5320   -1-1->wf1 5321

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 5329

This theorem is referenced by:  f1rn  5540  f1fn  5541  f1ss  5545  f1ssres  5548  f1of  5580  dff1o5  5589  fsnd  5624  cocan1  5923  f1o2ndf1  6388  brdomg  6914  f1dom2g  6924  f1domg  6926  dom3d  6942  f1imaen2g  6962  2dom  6975  1dom1el  6988  dom1o  6997  xpdom2  7010  dom0  7019  phplem4dom  7043  isinfinf  7079  infm  7089  updjudhcoinlf  7270  updjudhcoinrg  7271  casef1  7280  djudom  7283  difinfsnlem  7289  difinfsn  7290  seqf1oglem1  10771  fihashf1rn  11040  ennnfonelemrn  13030  reeff1o  15487  ushgruhgr  15921  umgr0e  15959  usgredgssen  16001  ausgrusgrben  16007  usgrss  16016  uspgrupgr  16020  usgrumgr  16023  usgrislfuspgrdom  16029  ushgredgedg  16065  ushgredgedgloop  16067  3dom  16523  pwle2  16535