Theorem f1f 5573

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 5357	. 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 4748   Fun wfun 5346   -->wf 5348   -1-1->wf1 5349

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 5357

This theorem is referenced by:  f1rn  5574  f1fn  5575  f1ss  5579  f1ssres  5582  f1of  5614  dff1o5  5623  fsnd  5659  cocan1  5960  f1o2ndf1  6424  brdomg  6985  f1dom2g  6995  f1domg  6997  dom3d  7013  f1imaen2g  7033  2dom  7046  1dom1el  7060  dom1o  7069  xpdom2  7082  dom0  7091  phplem4dom  7116  isinfinf  7154  infm  7164  updjudhcoinlf  7371  updjudhcoinrg  7372  casef1  7381  djudom  7384  difinfsnlem  7390  difinfsn  7391  seqf1oglem1  10881  fihashf1rn  11151  ennnfonelemrn  13170  reeff1o  15638  ushgruhgr  16075  umgr0e  16113  usgredgssen  16157  ausgrusgrben  16163  usgrss  16172  uspgrupgr  16176  usgrumgr  16179  usgrislfuspgrdom  16185  ushgredgedg  16221  ushgredgedgloop  16223  trlsegvdeglem6  16460  trlsegvdeglem7  16461  trlsegvdegfi  16462  eupth2lem3lem2fi  16464  eupth2lem3lem3fi  16465  eupth2lem3lem6fi  16466  eupth2lem3lem4fi  16468  3dom  16762  pwle2  16772