Theorem f1f 6568

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 6353	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
2	1	simplbi 500	1 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵)

Syntax hints:   → wi 4  ^◡ccnv 5547  Fun wfun 6342  ⟶wf 6344  –1-1→wf1 6345

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 209  df-an 399  df-f1 6353

This theorem is referenced by:  f1fn  6569  f1ss  6573  f1ssres  6575  f1of  6608  dff1o5  6617  fsnd  6650  f1cofveqaeq  7009  f1cofveqaeqALT  7010  2f1fvneq  7011  f1dom3el3dif  7020  f1prex  7033  cocan1  7040  f1iun  7638  f1dmex  7651  f1o2ndf1  7811  oacomf1olem  8183  brdomg  8512  f1dom2g  8520  f1domg  8522  dom3d  8544  f1imaen2g  8563  2dom  8575  domdifsn  8593  xpdom2  8605  domunsncan  8610  fodomr  8661  domss2  8669  domssex2  8670  sucdom2  8707  f1finf1o  8738  f1fi  8804  oiexg  8992  hartogslem1  8999  infdifsn  9113  fseqenlem1  9443  fseqenlem2  9444  ac10ct  9453  acndom  9470  acndom2  9473  dfac12lem2  9563  dfac12lem3  9564  ackbij1  9653  fictb  9660  cfsmolem  9685  cfcoflem  9687  cfcof  9689  fin23lem17  9753  fin23lem32  9759  fin23lem39  9765  fin23lem41  9767  fin1a2lem6  9820  fin1a2lem7  9821  iundom2g  9955  alephreg  9997  canthnumlem  10063  canthwelem  10065  pwfseqlem1  10073  pwfseqlem5  10078  seqf1olem1  13406  hashf1rn  13710  hashimarn  13798  hashf1lem1  13810  hashf1lem2  13811  cshf1  14167  setcmon  17342  injsubmefmnd  18057  odinf  18685  odcl2  18687  sylow1lem2  18719  gsumval3lem1  19020  gsumval3lem2  19021  gsumval3  19022  gsumzcl2  19025  gsumzf1o  19027  gsumzaddlem  19036  gsumzmhm  19052  gsumzoppg  19059  dprdf1  19150  f1lindf  20961  f1linds  20964  lindfmm  20966  mdetunilem8  21223  2ndcdisj  22059  itg1addlem4  24295  reeff1o  25033  birthdaylem1  25527  dchrisum0fno1  26085  ushgruhgr  26852  umgr0e  26893  usgredgss  26942  ausgrusgrb  26948  usgrss  26957  uspgrupgr  26959  usgrumgr  26962  usgruspgrb  26964  usgrislfuspgr  26967  usgredg2ALT  26973  ushgredgedg  27009  ushgredgedgloop  27011  usgr2pth  27543  0wlkons1  27898  trlsegvdeg  28004  fsumiunle  30545  cycpmco2lem1  30789  cycpmco2lem5  30793  cycpmco2  30796  cycpmconjv  30805  cyc3conja  30820  qqhre  31282  esumiun  31374  hashf1dmcdm  32377  erdszelem4  32462  erdszelem8  32466  erdszelem9  32467  erdsze2lem2  32472  pibt2  34722  diophrw  39432  eldioph2lem2  39434  eldioph2  39435  eldioph2b  39436  dnwech  39724  seff  40715  fargshiftf1  43675  fmtnoinf  43772  ushrisomgr  44080