Theorem f1f 6738

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

Syntax hints:   → wi 4  ^◡ccnv 5631  Fun wfun 6494  ⟶wf 6496  –1-1→wf1 6497

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 207  df-an 396  df-f1 6505

This theorem is referenced by:  f1fn  6739  f1ss  6743  f1ssres  6745  f1co  6749  f1of  6782  dff1o5  6791  f1un  6802  fsnd  6826  f1cofveqaeq  7213  f1cofveqaeqALT  7214  2f1fvneq  7216  f1dom3el3dif  7225  f1cdmsn  7238  f1prex  7240  cocan1  7247  fvf1pr  7263  f1iun  7898  f1dmex  7911  f1o2ndf1  8074  oacomf1olem  8501  brdomg  8907  f1dom2g  8918  f1domg  8920  dom3d  8943  f1imaen2g  8964  2dom  8979  domdifsn  9000  xpdom2  9012  domunsncan  9017  dom0  9045  fodomr  9068  domss2  9076  domssex2  9077  f1domfi  9117  sucdom2  9139  f1finf1o  9185  infn0  9214  f1fi  9226  fodomfir  9240  oiexg  9452  hartogslem1  9459  infdifsn  9578  fseqenlem1  9946  fseqenlem2  9947  ac10ct  9956  acndom  9973  acndom2  9976  dfac12lem2  10067  dfac12lem3  10068  ackbij1  10159  fictb  10166  cfsmolem  10192  cfcoflem  10194  cfcof  10196  fin23lem17  10260  fin23lem32  10266  fin23lem39  10272  fin23lem41  10274  fin1a2lem6  10327  fin1a2lem7  10328  iundom2g  10462  alephreg  10505  canthnumlem  10571  canthwelem  10573  pwfseqlem1  10581  pwfseqlem5  10586  fvf1tp  13721  seqf1olem1  13976  hashf1rn  14287  hashimarn  14375  hashf1dmcdm  14379  hashf1lem1  14390  hashf1lem2  14391  cshf1  14745  setcmon  18023  injsubmefmnd  18834  odinf  19504  odcl2  19506  sylow1lem2  19540  gsumval3lem1  19846  gsumval3lem2  19847  gsumval3  19848  gsumzcl2  19851  gsumzf1o  19853  gsumzaddlem  19862  gsumzmhm  19878  gsumzoppg  19885  dprdf1  19976  f1lindf  21789  f1linds  21792  lindfmm  21794  mdetunilem8  22575  2ndcdisj  23412  itg1addlem4  25668  reeff1o  26425  birthdaylem1  26929  dchrisum0fno1  27490  ushgruhgr  29154  umgr0e  29195  usgredgss  29244  ausgrusgrb  29250  usgrss  29259  uspgrupgr  29263  usgrumgr  29266  usgruspgrb  29268  usgrislfuspgr  29272  usgredg2ALT  29278  ushgredgedg  29314  ushgredgedgloop  29316  usgr2pth  29849  0wlkons1  30208  trlsegvdeg  30314  fsumiunle  32920  cycpmco2lem1  33219  cycpmco2lem5  33223  cycpmco2  33226  cycpmconjv  33235  cyc3conja  33250  idomsubr  33402  islbs5  33472  extdgfialglem1  33869  qqhre  34197  esumiun  34271  erdszelem4  35407  erdszelem8  35411  erdszelem9  35412  erdsze2lem2  35417  pibt2  37666  aks6d1c2  42494  aks6d1c6lem3  42536  diophrw  43110  eldioph2lem2  43112  eldioph2  43113  eldioph2b  43114  dnwech  43399  cantnfub2  43673  seff  44659  fargshiftf1  47795  fmtnoinf  47890  upgrimtrlslem2  48259  ushggricedg  48281  grtrimap  48302  oppff1o  49502  fucoppcid  49761  diag1f1o  49887  diag2f1o  49890