Theorem f1f 6014

Description: A one-to-one mapping is a mapping. (Contributed by NM, 31-Dec-1996.)

Assertion

Ref	Expression
f1f	⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵)

Proof of Theorem f1f

Step	Hyp	Ref	Expression
1		df-f1 5809	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
2	1	simplbi 475	1 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵)

Syntax hints:   → wi 4  ^◡ccnv 5037  Fun wfun 5798  ⟶wf 5800  –1-1→wf1 5801

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 196  df-an 385  df-f1 5809

This theorem is referenced by:  f1fn  6015  f1ss  6019  f1ssres  6021  f1of  6050  dff1o5  6059  fsnd  6091  f1dom3el3dif  6426  f1prex  6439  cocan1  6446  fun11iun  7019  f1dmex  7029  f1o2ndf1  7172  oacomf1olem  7531  brdomg  7851  f1dom2g  7859  f1domg  7861  dom3d  7883  f1imaen2g  7903  2dom  7915  domdifsn  7928  xpdom2  7940  domunsncan  7945  fodomr  7996  domss2  8004  domssex2  8005  sucdom2  8041  f1finf1o  8072  f1fi  8136  oiexg  8323  hartogslem1  8330  infdifsn  8437  fseqenlem1  8730  fseqenlem2  8731  ac10ct  8740  acndom  8757  acndom2  8760  dfac12lem2  8849  dfac12lem3  8850  ackbij1  8943  fictb  8950  cfsmolem  8975  cfcoflem  8977  cfcof  8979  fin23lem17  9043  fin23lem32  9049  fin23lem39  9055  fin23lem41  9057  fin1a2lem6  9110  fin1a2lem7  9111  iundom2g  9241  alephreg  9283  canthnumlem  9349  canthwelem  9351  pwfseqlem1  9359  pwfseqlem5  9364  seqf1olem1  12702  hashf1rn  13004  hashf1rnOLD  13005  hashimarn  13085  hashf1lem1  13096  hashf1lem2  13097  cshf1  13407  setcmon  16560  odinf  17803  odcl2  17805  odf1o1  17810  sylow1lem2  17837  gsumval3lem1  18129  gsumval3lem2  18130  gsumval3  18131  gsumzcl2  18134  gsumzf1o  18136  gsumzaddlem  18144  gsumzmhm  18160  gsumzoppg  18167  dprdf1  18255  f1lindf  19980  f1linds  19983  lindfmm  19985  mdetunilem8  20244  2ndcdisj  21069  itg1addlem4  23272  reeff1o  24005  birthdaylem1  24478  basellem3  24609  dchrisum0fno1  25000  ushgruhgr  25735  umgr0e  25776  ushgrauhgra  25832  edgss  25881  ausisusgra  25884  usgrass  25890  uslisumgra  25893  usgra0v  25900  usgraedg2  25904  usgraedgrnv  25906  usgrarnedg  25913  usgraedg4  25916  usgra1v  25919  usgrares1  25939  cusgrarn  25988  fargshiftf1  26165  usgrcyclnl2  26169  clwlkisclwwlklem1  26315  usgravd00  26446  qqhre  29392  esumiun  29483  erdszelem4  30430  erdszelem8  30434  erdszelem9  30435  erdsze2lem2  30440  diophrw  36340  eldioph2lem2  36342  eldioph2  36343  eldioph2b  36344  dnwech  36636  seff  37530  fmtnoinf  39986  2f1fvneq  40322  f1cofveqaeq  40323  f1cofveqaeqALT  40324  usgredgss  40390  ausgrusgrb  40395  usgrss  40404  uspgrupgr  40406  usgrumgr  40409  usgruspgrb  40411  usgrislfuspgr  40414  usgredg2ALT  40420  ushgredgedga  40456  ushgredgedgaloop  40458  usgr2pth  40970  0wlkOns1  41289  trlsegvdeg  41395