Theorem f1f 6720

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

Syntax hints:   → wi 4  ^◡ccnv 5618  Fun wfun 6476  ⟶wf 6478  –1-1→wf1 6479

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 6487

This theorem is referenced by:  f1fn  6721  f1ss  6725  f1ssres  6727  f1co  6731  f1of  6764  dff1o5  6773  f1un  6784  fsnd  6807  f1cofveqaeq  7194  f1cofveqaeqALT  7195  2f1fvneq  7197  f1dom3el3dif  7206  f1cdmsn  7219  f1prex  7221  cocan1  7228  fvf1pr  7244  f1iun  7879  f1dmex  7892  f1o2ndf1  8055  oacomf1olem  8482  brdomg  8884  f1dom2g  8895  f1domg  8897  dom3d  8919  f1imaen2g  8940  2dom  8955  domdifsn  8977  xpdom2  8989  domunsncan  8994  dom0  9022  fodomr  9045  domss2  9053  domssex2  9054  f1domfi  9095  sucdom2  9117  f1finf1o  9162  infn0  9191  f1fi  9203  fodomfir  9218  oiexg  9427  hartogslem1  9434  infdifsn  9553  fseqenlem1  9918  fseqenlem2  9919  ac10ct  9928  acndom  9945  acndom2  9948  dfac12lem2  10039  dfac12lem3  10040  ackbij1  10131  fictb  10138  cfsmolem  10164  cfcoflem  10166  cfcof  10168  fin23lem17  10232  fin23lem32  10238  fin23lem39  10244  fin23lem41  10246  fin1a2lem6  10299  fin1a2lem7  10300  iundom2g  10434  alephreg  10476  canthnumlem  10542  canthwelem  10544  pwfseqlem1  10552  pwfseqlem5  10557  fvf1tp  13693  seqf1olem1  13948  hashf1rn  14259  hashimarn  14347  hashf1dmcdm  14351  hashf1lem1  14362  hashf1lem2  14363  cshf1  14716  setcmon  17994  injsubmefmnd  18771  odinf  19442  odcl2  19444  sylow1lem2  19478  gsumval3lem1  19784  gsumval3lem2  19785  gsumval3  19786  gsumzcl2  19789  gsumzf1o  19791  gsumzaddlem  19800  gsumzmhm  19816  gsumzoppg  19823  dprdf1  19914  f1lindf  21729  f1linds  21732  lindfmm  21734  mdetunilem8  22504  2ndcdisj  23341  itg1addlem4  25598  reeff1o  26355  birthdaylem1  26859  dchrisum0fno1  27420  ushgruhgr  29018  umgr0e  29059  usgredgss  29108  ausgrusgrb  29114  usgrss  29123  uspgrupgr  29127  usgrumgr  29130  usgruspgrb  29132  usgrislfuspgr  29136  usgredg2ALT  29142  ushgredgedg  29178  ushgredgedgloop  29180  usgr2pth  29713  0wlkons1  30069  trlsegvdeg  30175  fsumiunle  32783  cycpmco2lem1  33077  cycpmco2lem5  33081  cycpmco2  33084  cycpmconjv  33093  cyc3conja  33108  idomsubr  33257  islbs5  33326  extdgfialglem1  33675  qqhre  34003  esumiun  34077  erdszelem4  35187  erdszelem8  35191  erdszelem9  35192  erdsze2lem2  35197  pibt2  37411  aks6d1c2  42123  aks6d1c6lem3  42165  diophrw  42752  eldioph2lem2  42754  eldioph2  42755  eldioph2b  42756  dnwech  43041  cantnfub2  43315  seff  44302  fargshiftf1  47445  fmtnoinf  47540  upgrimtrlslem2  47909  ushggricedg  47931  grtrimap  47952  oppff1o  49154  fucoppcid  49413  diag1f1o  49539  diag2f1o  49542