Theorem f1f 6569

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

Syntax hints:   → wi 4  ^◡ccnv 5548  Fun wfun 6343  ⟶wf 6345  –1-1→wf1 6346

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 6354

This theorem is referenced by:  f1fn  6570  f1ss  6574  f1ssres  6576  f1of  6609  dff1o5  6618  fsnd  6651  f1cofveqaeq  7010  f1cofveqaeqALT  7011  2f1fvneq  7012  f1dom3el3dif  7021  f1prex  7034  cocan1  7041  f1iun  7639  f1dmex  7652  f1o2ndf1  7812  oacomf1olem  8184  brdomg  8513  f1dom2g  8521  f1domg  8523  dom3d  8545  f1imaen2g  8564  2dom  8576  domdifsn  8594  xpdom2  8606  domunsncan  8611  fodomr  8662  domss2  8670  domssex2  8671  sucdom2  8708  f1finf1o  8739  f1fi  8805  oiexg  8993  hartogslem1  9000  infdifsn  9114  fseqenlem1  9444  fseqenlem2  9445  ac10ct  9454  acndom  9471  acndom2  9474  dfac12lem2  9564  dfac12lem3  9565  ackbij1  9654  fictb  9661  cfsmolem  9686  cfcoflem  9688  cfcof  9690  fin23lem17  9754  fin23lem32  9760  fin23lem39  9766  fin23lem41  9768  fin1a2lem6  9821  fin1a2lem7  9822  iundom2g  9956  alephreg  9998  canthnumlem  10064  canthwelem  10066  pwfseqlem1  10074  pwfseqlem5  10079  seqf1olem1  13403  hashf1rn  13707  hashimarn  13795  hashf1lem1  13807  hashf1lem2  13808  cshf1  14166  setcmon  17341  injsubmefmnd  18056  odinf  18684  odcl2  18686  sylow1lem2  18718  gsumval3lem1  19019  gsumval3lem2  19020  gsumval3  19021  gsumzcl2  19024  gsumzf1o  19026  gsumzaddlem  19035  gsumzmhm  19051  gsumzoppg  19058  dprdf1  19149  f1lindf  20960  f1linds  20963  lindfmm  20965  mdetunilem8  21222  2ndcdisj  22058  itg1addlem4  24294  reeff1o  25029  birthdaylem1  25523  dchrisum0fno1  26081  ushgruhgr  26848  umgr0e  26889  usgredgss  26938  ausgrusgrb  26944  usgrss  26953  uspgrupgr  26955  usgrumgr  26958  usgruspgrb  26960  usgrislfuspgr  26963  usgredg2ALT  26969  ushgredgedg  27005  ushgredgedgloop  27007  usgr2pth  27539  0wlkons1  27894  trlsegvdeg  28000  fsumiunle  30540  cycpmco2lem1  30763  cycpmco2lem5  30767  cycpmco2  30770  cycpmconjv  30779  cyc3conja  30794  qqhre  31256  esumiun  31348  hashf1dmcdm  32351  erdszelem4  32436  erdszelem8  32440  erdszelem9  32441  erdsze2lem2  32446  pibt2  34692  diophrw  39349  eldioph2lem2  39351  eldioph2  39352  eldioph2b  39353  dnwech  39641  seff  40634  fargshiftf1  43595  fmtnoinf  43692  ushrisomgr  44000