Theorem f1f 5210

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 5015	. 2 |- ( F : A -1-1-> B <-> ( F : A --> B /\ Fun `' F ) )
2	1	simplbi 268	1 |- ( F : A -1-1-> B -> F : A --> B )

Syntax hints:   -> wi 4   `'ccnv 4435   Fun wfun 5004   -->wf 5006   -1-1->wf1 5007

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104

This theorem depends on definitions:  df-bi 115  df-f1 5015

This theorem is referenced by:  f1rn  5211  f1fn  5212  f1ss  5216  f1ssres  5219  f1of  5247  dff1o5  5256  cocan1  5558  f1o2ndf1  5985  brdomg  6455  f1dom2g  6463  f1domg  6465  dom3d  6481  f1imaen2g  6500  2dom  6512  xpdom2  6537  dom0  6544  phplem4dom  6568  isinfinf  6603  infm  6610  updjudhcoinlf  6761  updjudhcoinrg  6762  casef1  6771  djudom  6777  fihashf1rn  10185