Theorem f1f 6101

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 5893	. 2 |- ( F : A -1-1-> B <-> ( F : A --> B /\ Fun `' F ) )
2	1	simplbi 476	1 |- ( F : A -1-1-> B -> F : A --> B )

Syntax hints:   -> wi 4   `'ccnv 5113   Fun wfun 5882   -->wf 5884   -1-1->wf1 5885

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386  df-f1 5893

This theorem is referenced by:  f1fn  6102  f1ss  6106  f1ssres  6108  f1of  6137  dff1o5  6146  fsnd  6179  f1cofveqaeq  6515  f1cofveqaeqALT  6516  2f1fvneq  6517  f1dom3el3dif  6526  f1prex  6539  cocan1  6546  fun11iun  7126  f1dmex  7136  f1o2ndf1  7285  oacomf1olem  7644  brdomg  7965  f1dom2g  7973  f1domg  7975  dom3d  7997  f1imaen2g  8017  2dom  8029  domdifsn  8043  xpdom2  8055  domunsncan  8060  fodomr  8111  domss2  8119  domssex2  8120  sucdom2  8156  f1finf1o  8187  f1fi  8253  oiexg  8440  hartogslem1  8447  infdifsn  8554  fseqenlem1  8847  fseqenlem2  8848  ac10ct  8857  acndom  8874  acndom2  8877  dfac12lem2  8966  dfac12lem3  8967  ackbij1  9060  fictb  9067  cfsmolem  9092  cfcoflem  9094  cfcof  9096  fin23lem17  9160  fin23lem32  9166  fin23lem39  9172  fin23lem41  9174  fin1a2lem6  9227  fin1a2lem7  9228  iundom2g  9362  alephreg  9404  canthnumlem  9470  canthwelem  9472  pwfseqlem1  9480  pwfseqlem5  9485  seqf1olem1  12840  hashf1rn  13142  hashf1rnOLD  13143  hashimarn  13227  hashf1lem1  13239  hashf1lem2  13240  cshf1  13556  setcmon  16737  odinf  17980  odcl2  17982  odf1o1  17987  sylow1lem2  18014  gsumval3lem1  18306  gsumval3lem2  18307  gsumval3  18308  gsumzcl2  18311  gsumzf1o  18313  gsumzaddlem  18321  gsumzmhm  18337  gsumzoppg  18344  dprdf1  18432  f1lindf  20161  f1linds  20164  lindfmm  20166  mdetunilem8  20425  2ndcdisj  21259  itg1addlem4  23466  reeff1o  24201  birthdaylem1  24678  basellem3  24809  dchrisum0fno1  25200  ushgruhgr  25964  umgr0e  26005  usgredgss  26054  ausgrusgrb  26060  usgrss  26069  uspgrupgr  26071  usgrumgr  26074  usgruspgrb  26076  usgrislfuspgr  26079  usgredg2ALT  26085  ushgredgedg  26121  ushgredgedgloop  26123  usgr2pth  26660  0wlkons1  26982  trlsegvdeg  27087  fsumiunle  29575  qqhre  30064  esumiun  30156  erdszelem4  31176  erdszelem8  31180  erdszelem9  31181  erdsze2lem2  31186  diophrw  37322  eldioph2lem2  37324  eldioph2  37325  eldioph2b  37326  dnwech  37618  seff  38508  fargshiftf1  41377  fmtnoinf  41448