Theorem f1f 6654

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

Syntax hints:   → wi 4  ^◡ccnv 5579  Fun wfun 6412  ⟶wf 6414  –1-1→wf1 6415

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 206  df-an 396  df-f1 6423

This theorem is referenced by:  f1fn  6655  f1ss  6660  f1ssres  6662  f1co  6666  f1of  6700  dff1o5  6709  fsnd  6742  f1cofveqaeq  7112  f1cofveqaeqALT  7113  2f1fvneq  7114  f1dom3el3dif  7123  f1prex  7136  cocan1  7143  f1iun  7760  f1dmex  7773  f1o2ndf1  7934  oacomf1olem  8357  brdomg  8703  f1dom2g  8712  f1dom2gOLD  8713  f1domg  8715  dom3d  8737  f1imaen2g  8756  2dom  8774  domdifsn  8795  xpdom2  8807  domunsncan  8812  sucdom2  8822  fodomr  8864  domss2  8872  domssex2  8873  f1domfi  8928  f1finf1o  8975  f1fi  9036  oiexg  9224  hartogslem1  9231  infdifsn  9345  fseqenlem1  9711  fseqenlem2  9712  ac10ct  9721  acndom  9738  acndom2  9741  dfac12lem2  9831  dfac12lem3  9832  ackbij1  9925  fictb  9932  cfsmolem  9957  cfcoflem  9959  cfcof  9961  fin23lem17  10025  fin23lem32  10031  fin23lem39  10037  fin23lem41  10039  fin1a2lem6  10092  fin1a2lem7  10093  iundom2g  10227  alephreg  10269  canthnumlem  10335  canthwelem  10337  pwfseqlem1  10345  pwfseqlem5  10350  seqf1olem1  13690  hashf1rn  13995  hashimarn  14083  hashf1lem1  14096  hashf1lem1OLD  14097  hashf1lem2  14098  cshf1  14451  setcmon  17718  injsubmefmnd  18451  odinf  19085  odcl2  19087  sylow1lem2  19119  gsumval3lem1  19421  gsumval3lem2  19422  gsumval3  19423  gsumzcl2  19426  gsumzf1o  19428  gsumzaddlem  19437  gsumzmhm  19453  gsumzoppg  19460  dprdf1  19551  f1lindf  20939  f1linds  20942  lindfmm  20944  mdetunilem8  21676  2ndcdisj  22515  itg1addlem4  24768  itg1addlem4OLD  24769  reeff1o  25511  birthdaylem1  26006  dchrisum0fno1  26564  ushgruhgr  27342  umgr0e  27383  usgredgss  27432  ausgrusgrb  27438  usgrss  27447  uspgrupgr  27449  usgrumgr  27452  usgruspgrb  27454  usgrislfuspgr  27457  usgredg2ALT  27463  ushgredgedg  27499  ushgredgedgloop  27501  usgr2pth  28033  0wlkons1  28386  trlsegvdeg  28492  fsumiunle  31045  cycpmco2lem1  31295  cycpmco2lem5  31299  cycpmco2  31302  cycpmconjv  31311  cyc3conja  31326  qqhre  31870  esumiun  31962  hashf1dmcdm  32976  erdszelem4  33056  erdszelem8  33060  erdszelem9  33061  erdsze2lem2  33066  pibt2  35515  diophrw  40497  eldioph2lem2  40499  eldioph2  40500  eldioph2b  40501  dnwech  40789  seff  41816  fargshiftf1  44781  fmtnoinf  44876  ushrisomgr  45181