Theorem f1f 5413

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 5213	. 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 4619   Fun wfun 5202   -->wf 5204   -1-1->wf1 5205

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 5213

This theorem is referenced by:  f1rn  5414  f1fn  5415  f1ss  5419  f1ssres  5422  f1of  5453  dff1o5  5462  fsnd  5496  cocan1  5778  f1o2ndf1  6219  brdomg  6738  f1dom2g  6746  f1domg  6748  dom3d  6764  f1imaen2g  6783  2dom  6795  xpdom2  6821  dom0  6828  phplem4dom  6852  isinfinf  6887  infm  6894  updjudhcoinlf  7069  updjudhcoinrg  7070  casef1  7079  djudom  7082  difinfsnlem  7088  difinfsn  7089  fihashf1rn  10736  ennnfonelemrn  12387  reeff1o  13774  pwle2  14317