Theorem f1f 5464

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 5264	. 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 4663   Fun wfun 5253   -->wf 5255   -1-1->wf1 5256

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 5264

This theorem is referenced by:  f1rn  5465  f1fn  5466  f1ss  5470  f1ssres  5473  f1of  5505  dff1o5  5514  fsnd  5548  cocan1  5835  f1o2ndf1  6287  brdomg  6808  f1dom2g  6816  f1domg  6818  dom3d  6834  f1imaen2g  6853  2dom  6865  xpdom2  6891  dom0  6900  phplem4dom  6924  isinfinf  6959  infm  6966  updjudhcoinlf  7147  updjudhcoinrg  7148  casef1  7157  djudom  7160  difinfsnlem  7166  difinfsn  7167  seqf1oglem1  10613  fihashf1rn  10882  ennnfonelemrn  12646  reeff1o  15019  1dom1el  15647  pwle2  15653