Theorem f1f 5481

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 5276	. 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 4674   Fun wfun 5265   -->wf 5267   -1-1->wf1 5268

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 5276

This theorem is referenced by:  f1rn  5482  f1fn  5483  f1ss  5487  f1ssres  5490  f1of  5522  dff1o5  5531  fsnd  5565  cocan1  5856  f1o2ndf1  6314  brdomg  6837  f1dom2g  6847  f1domg  6849  dom3d  6865  f1imaen2g  6885  2dom  6897  xpdom2  6926  dom0  6935  phplem4dom  6959  isinfinf  6994  infm  7001  updjudhcoinlf  7182  updjudhcoinrg  7183  casef1  7192  djudom  7195  difinfsnlem  7201  difinfsn  7202  seqf1oglem1  10664  fihashf1rn  10933  ennnfonelemrn  12790  reeff1o  15245  1dom1el  15927  pwle2  15935