Theorem f1f 5466

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  5467  f1fn  5468  f1ss  5472  f1ssres  5475  f1of  5507  dff1o5  5516  fsnd  5550  cocan1  5837  f1o2ndf1  6295  brdomg  6816  f1dom2g  6824  f1domg  6826  dom3d  6842  f1imaen2g  6861  2dom  6873  xpdom2  6899  dom0  6908  phplem4dom  6932  isinfinf  6967  infm  6974  updjudhcoinlf  7155  updjudhcoinrg  7156  casef1  7165  djudom  7168  difinfsnlem  7174  difinfsn  7175  seqf1oglem1  10630  fihashf1rn  10899  ennnfonelemrn  12663  reeff1o  15095  1dom1el  15723  pwle2  15731