Theorem f1f 6798

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

Syntax hints:   → wi 4  ^◡ccnv 5681  Fun wfun 6548  ⟶wf 6550  –1-1→wf1 6551

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 206  df-an 395  df-f1 6559

This theorem is referenced by:  f1fn  6799  f1ss  6803  f1ssres  6805  f1co  6809  f1of  6843  dff1o5  6852  f1un  6863  fsnd  6886  f1cofveqaeq  7273  f1cofveqaeqALT  7274  2f1fvneq  7275  f1dom3el3dif  7284  f1cdmsn  7296  f1prex  7298  cocan1  7305  f1iun  7957  f1dmex  7970  f1o2ndf1  8136  oacomf1olem  8594  brdomg  8987  brdomgOLD  8988  f1dom2g  9000  f1dom2gOLD  9001  f1domg  9003  dom3d  9025  f1imaen2g  9046  2dom  9066  domdifsn  9092  xpdom2  9105  domunsncan  9110  sucdom2OLD  9120  dom0  9140  fodomr  9166  domss2  9174  domssex2  9175  f1domfi  9218  sucdom2  9240  f1finf1o  9305  f1finf1oOLD  9306  infn0  9341  f1fi  9354  fodomfir  9370  oiexg  9578  hartogslem1  9585  infdifsn  9700  fseqenlem1  10067  fseqenlem2  10068  ac10ct  10077  acndom  10094  acndom2  10097  dfac12lem2  10187  dfac12lem3  10188  ackbij1  10281  fictb  10288  cfsmolem  10313  cfcoflem  10315  cfcof  10317  fin23lem17  10381  fin23lem32  10387  fin23lem39  10393  fin23lem41  10395  fin1a2lem6  10448  fin1a2lem7  10449  iundom2g  10583  alephreg  10625  canthnumlem  10691  canthwelem  10693  pwfseqlem1  10701  pwfseqlem5  10706  seqf1olem1  14061  hashf1rn  14369  hashimarn  14457  hashf1dmcdm  14461  hashf1lem1  14473  hashf1lem1OLD  14474  hashf1lem2  14475  cshf1  14818  setcmon  18109  injsubmefmnd  18887  odinf  19561  odcl2  19563  sylow1lem2  19597  gsumval3lem1  19903  gsumval3lem2  19904  gsumval3  19905  gsumzcl2  19908  gsumzf1o  19910  gsumzaddlem  19919  gsumzmhm  19935  gsumzoppg  19942  dprdf1  20033  f1lindf  21820  f1linds  21823  lindfmm  21825  mdetunilem8  22612  2ndcdisj  23451  itg1addlem4  25719  itg1addlem4OLD  25720  reeff1o  26477  birthdaylem1  26979  dchrisum0fno1  27540  ushgruhgr  29005  umgr0e  29046  usgredgss  29095  ausgrusgrb  29101  usgrss  29110  uspgrupgr  29114  usgrumgr  29117  usgruspgrb  29119  usgrislfuspgr  29123  usgredg2ALT  29129  ushgredgedg  29165  ushgredgedgloop  29167  usgr2pth  29701  0wlkons1  30054  trlsegvdeg  30160  fsumiunle  32730  cycpmco2lem1  33004  cycpmco2lem5  33008  cycpmco2  33011  cycpmconjv  33020  cyc3conja  33035  idomsubr  33159  islbs5  33255  qqhre  33835  esumiun  33927  erdszelem4  35022  erdszelem8  35026  erdszelem9  35027  erdsze2lem2  35032  pibt2  37124  aks6d1c2  41828  aks6d1c6lem3  41870  diophrw  42416  eldioph2lem2  42418  eldioph2  42419  eldioph2b  42420  dnwech  42709  cantnfub2  42988  seff  43983  fargshiftf1  47013  fmtnoinf  47108  ushggricedg  47475