Theorem f1f 5503

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 5295	. 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 4692   Fun wfun 5284   -->wf 5286   -1-1->wf1 5287

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 5295

This theorem is referenced by:  f1rn  5504  f1fn  5505  f1ss  5509  f1ssres  5512  f1of  5544  dff1o5  5553  fsnd  5588  cocan1  5879  f1o2ndf1  6337  brdomg  6860  f1dom2g  6870  f1domg  6872  dom3d  6888  f1imaen2g  6908  2dom  6921  xpdom2  6951  dom0  6960  phplem4dom  6984  isinfinf  7020  infm  7027  updjudhcoinlf  7208  updjudhcoinrg  7209  casef1  7218  djudom  7221  difinfsnlem  7227  difinfsn  7228  seqf1oglem1  10701  fihashf1rn  10970  ennnfonelemrn  12905  reeff1o  15360  ushgruhgr  15791  umgr0e  15826  1dom1el  16126  dom1o  16128  pwle2  16137