Theorem f1f 5423

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 5223	. 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 4627   Fun wfun 5212   -->wf 5214   -1-1->wf1 5215

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 5223

This theorem is referenced by:  f1rn  5424  f1fn  5425  f1ss  5429  f1ssres  5432  f1of  5463  dff1o5  5472  fsnd  5506  cocan1  5790  f1o2ndf1  6231  brdomg  6750  f1dom2g  6758  f1domg  6760  dom3d  6776  f1imaen2g  6795  2dom  6807  xpdom2  6833  dom0  6840  phplem4dom  6864  isinfinf  6899  infm  6906  updjudhcoinlf  7081  updjudhcoinrg  7082  casef1  7091  djudom  7094  difinfsnlem  7100  difinfsn  7101  fihashf1rn  10770  ennnfonelemrn  12422  reeff1o  14279  pwle2  14833