Theorem f1f 6726

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

Syntax hints:   → wi 4  ^◡ccnv 5619  Fun wfun 6482  ⟶wf 6484  –1-1→wf1 6485

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 398  df-f1 6493

This theorem is referenced by:  f1fn  6727  f1ss  6731  f1ssres  6733  f1co  6737  f1of  6770  dff1o5  6779  f1un  6790  fsnd  6814  f1cofveqaeq  7204  f1cofveqaeqALT  7205  2f1fvneq  7207  f1dom3el3dif  7216  f1cdmsn  7229  f1prex  7231  cocan1  7238  fvf1pr  7254  f1iun  7888  f1dmex  7901  f1o2ndf1  8063  oacomf1olem  8493  brdomg  8899  f1dom2g  8910  f1domg  8912  dom3d  8935  f1imaen2g  8956  2dom  8971  domdifsn  8992  xpdom2  9004  domunsncan  9009  dom0  9037  fodomr  9060  domss2  9068  domssex2  9069  f1domfi  9109  sucdom2  9131  f1finf1o  9177  infn0  9206  f1fi  9218  fodomfir  9232  oiexg  9444  hartogslem1  9451  infdifsn  9573  fseqenlem1  9941  fseqenlem2  9942  ac10ct  9951  acndom  9968  acndom2  9971  dfac12lem2  10062  dfac12lem3  10063  ackbij1  10154  fictb  10161  cfsmolem  10188  cfcoflem  10190  cfcof  10192  fin23lem17  10256  fin23lem32  10262  fin23lem39  10268  fin23lem41  10270  fin1a2lem6  10323  fin1a2lem7  10324  iundom2g  10458  alephreg  10501  canthnumlem  10567  canthwelem  10569  pwfseqlem1  10577  pwfseqlem5  10582  fvf1tp  13743  seqf1olem1  13998  hashf1rn  14309  hashimarn  14397  hashf1dmcdm  14401  hashf1lem1  14412  hashf1lem2  14413  cshf1  14767  setcmon  18049  injsubmefmnd  18860  odinf  19532  odcl2  19534  sylow1lem2  19568  gsumval3lem1  19874  gsumval3lem2  19875  gsumval3  19876  gsumzcl2  19879  gsumzf1o  19881  gsumzaddlem  19890  gsumzmhm  19906  gsumzoppg  19913  dprdf1  20004  f1lindf  21800  f1linds  21803  lindfmm  21805  mdetunilem8  22605  2ndcdisj  23442  itg1addlem4  25687  reeff1o  26433  birthdaylem1  26936  dchrisum0fno1  27495  ushgruhgr  29158  umgr0e  29199  usgredgss  29248  ausgrusgrb  29254  usgrss  29263  uspgrupgr  29267  usgrumgr  29270  usgruspgrb  29272  usgrislfuspgr  29276  usgredg2ALT  29282  ushgredgedg  29318  ushgredgedgloop  29320  usgr2pth  29852  0wlkons1  30211  trlsegvdeg  30317  fsumiunle  32923  cycpmco2lem1  33209  cycpmco2lem5  33213  cycpmco2  33216  cycpmconjv  33225  cyc3conja  33240  idomsubr  33395  islbs5  33465  extdgfialglem1  33886  qqhre  34214  esumiun  34288  erdszelem4  35435  erdszelem8  35439  erdszelem9  35440  erdsze2lem2  35445  mh-inf3f1  36782  pibt2  37792  aks6d1c2  42628  aks6d1c6lem3  42670  diophrw  43221  eldioph2lem2  43223  eldioph2  43224  eldioph2b  43225  dnwech  43506  cantnfub2  43780  seff  44766  fargshiftf1  47928  fmtnoinf  48026  upgrimtrlslem2  48408  ushggricedg  48430  grtrimap  48451  oppff1o  49651  fucoppcid  49910  diag1f1o  50036  diag2f1o  50039