Theorem f1f 6730

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

Syntax hints:   → wi 4  ^◡ccnv 5624  Fun wfun 6486  ⟶wf 6488  –1-1→wf1 6489

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 208  df-an 397  df-f1 6497

This theorem is referenced by:  f1fn  6731  f1ss  6735  f1ssres  6737  f1co  6741  f1of  6774  dff1o5  6783  f1un  6794  fsnd  6818  f1cofveqaeq  7208  f1cofveqaeqALT  7209  2f1fvneq  7211  f1dom3el3dif  7220  f1cdmsn  7233  f1prex  7235  cocan1  7242  fvf1pr  7258  f1iun  7893  f1dmex  7906  f1o2ndf1  8068  oacomf1olem  8496  brdomg  8902  f1dom2g  8913  f1domg  8915  dom3d  8938  f1imaen2g  8959  2dom  8974  domdifsn  8995  xpdom2  9007  domunsncan  9012  dom0  9040  fodomr  9063  domss2  9071  domssex2  9072  f1domfi  9112  sucdom2  9134  f1finf1o  9180  infn0  9209  f1fi  9221  fodomfir  9235  oiexg  9447  hartogslem1  9454  infdifsn  9576  fseqenlem1  9944  fseqenlem2  9945  ac10ct  9954  acndom  9971  acndom2  9974  dfac12lem2  10065  dfac12lem3  10066  ackbij1  10157  fictb  10164  cfsmolem  10190  cfcoflem  10192  cfcof  10194  fin23lem17  10258  fin23lem32  10264  fin23lem39  10270  fin23lem41  10272  fin1a2lem6  10325  fin1a2lem7  10326  iundom2g  10460  alephreg  10503  canthnumlem  10569  canthwelem  10571  pwfseqlem1  10579  pwfseqlem5  10584  fvf1tp  13746  seqf1olem1  14001  hashf1rn  14312  hashimarn  14400  hashf1dmcdm  14404  hashf1lem1  14415  hashf1lem2  14416  cshf1  14770  setcmon  18052  injsubmefmnd  18863  odinf  19536  odcl2  19538  sylow1lem2  19572  gsumval3lem1  19878  gsumval3lem2  19879  gsumval3  19880  gsumzcl2  19883  gsumzf1o  19885  gsumzaddlem  19894  gsumzmhm  19910  gsumzoppg  19917  dprdf1  20008  f1lindf  21804  f1linds  21807  lindfmm  21809  mdetunilem8  22609  2ndcdisj  23446  itg1addlem4  25691  reeff1o  26437  birthdaylem1  26940  dchrisum0fno1  27499  ushgruhgr  29163  umgr0e  29204  usgredgss  29253  ausgrusgrb  29259  usgrss  29268  uspgrupgr  29272  usgrumgr  29275  usgruspgrb  29277  usgrislfuspgr  29281  usgredg2ALT  29287  ushgredgedg  29323  ushgredgedgloop  29325  usgr2pth  29857  0wlkons1  30216  trlsegvdeg  30322  fsumiunle  32928  cycpmco2lem1  33214  cycpmco2lem5  33218  cycpmco2  33221  cycpmconjv  33230  cyc3conja  33245  idomsubr  33400  islbs5  33470  extdgfialglem1  33883  qqhre  34211  esumiun  34285  erdszelem4  35429  erdszelem8  35433  erdszelem9  35434  erdsze2lem2  35439  mh-inf3f1  36776  pibt2  37786  aks6d1c2  42622  aks6d1c6lem3  42664  diophrw  43215  eldioph2lem2  43217  eldioph2  43218  eldioph2b  43219  dnwech  43500  cantnfub2  43774  seff  44760  fargshiftf1  47923  fmtnoinf  48021  upgrimtrlslem2  48403  ushggricedg  48425  grtrimap  48446  oppff1o  49646  fucoppcid  49905  diag1f1o  50031  diag2f1o  50034