Theorem f1f 6764

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

Syntax hints:   → wi 4  ^◡ccnv 5651  Fun wfun 6519  ⟶wf 6521  –1-1→wf1 6522

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 210  df-an 401  df-f1 6530

This theorem is referenced by:  f1fn  6765  f1rel  6768  f1ss  6771  f1ssres  6773  f1co  6777  f1of  6810  dff1o5  6820  f1un  6831  fsnd  6855  f1cofveqaeq  7245  f1cofveqaeqALT  7246  2f1fvneq  7248  f1dom3el3dif  7257  f1cdmsn  7270  f1prex  7272  cocan1  7279  fvf1pr  7295  f1iun  7929  f1dmex  7942  f1o2ndf1  8105  oacomf1olem  8537  brdomg  8943  f1dom2g  8954  f1domg  8956  dom3d  8979  f1imaen2g  9000  2dom  9015  domdifsn  9036  xpdom2  9048  domunsncan  9053  dom0  9081  fodomr  9104  domss2  9112  domssex2  9113  f1domfi  9153  sucdom2  9175  f1finf1o  9221  infn0  9250  f1fi  9262  fodomfir  9275  oiexg  9485  hartogslem1  9492  infdifsn  9614  fseqenlem1  9996  fseqenlem2  9997  ac10ct  10006  acndom  10023  acndom2  10026  dfac12lem2  10116  dfac12lem3  10117  ackbij1  10208  fictb  10215  cfsmolem  10242  cfcoflem  10244  cfcof  10246  fin23lem17  10310  fin23lem32  10316  fin23lem39  10322  fin23lem41  10324  fin1a2lem6  10377  fin1a2lem7  10378  iundom2g  10512  alephreg  10555  canthnumlem  10621  canthwelem  10623  pwfseqlem1  10631  pwfseqlem5  10636  fvf1tp  13813  seqf1olem1  14068  hashf1rn  14379  hashimarn  14467  hashf1dmcdm  14471  hashf1lem1  14482  hashf1lem2  14483  cshf1  14837  setcmon  18134  injsubmefmnd  18946  odinf  19624  odcl2  19626  sylow1lem2  19660  gsumval3lem1  19966  gsumval3lem2  19967  gsumval3  19968  gsumzcl2  19971  gsumzf1o  19973  gsumzaddlem  19982  gsumzmhm  19998  gsumzoppg  20005  dprdf1  20096  f1lindf  21932  f1linds  21935  lindfmm  21937  mdetunilem8  22737  2ndcdisj  23574  itg1addlem4  25819  reeff1o  26568  birthdaylem1  27074  dchrisum0fno1  27633  ushgruhgr  29328  umgr0e  29369  usgredgss  29418  ausgrusgrb  29424  usgrss  29433  uspgrupgr  29437  usgrumgr  29440  usgruspgrb  29442  usgrislfuspgr  29446  usgredg2ALT  29452  ushgredgedg  29488  ushgredgedgloop  29490  usgr2pth  30022  0wlkons1  30381  trlsegvdeg  30487  fsumiunle  33086  cycpmco2lem1  33359  cycpmco2lem5  33363  cycpmco2  33366  cycpmconjv  33375  cyc3conja  33390  idomsubr  33545  islbs5  33609  extdgfialglem1  33999  qqhre  34327  esumiun  34401  vonf1wev  35463  erdszelem4  35557  erdszelem8  35561  erdszelem9  35562  erdsze2lem2  35567  mh-inf3f1  36914  pibt2  37923  aks6d1c2  42759  aks6d1c6lem3  42801  diophrw  43352  eldioph2lem2  43354  eldioph2  43355  eldioph2b  43356  dnwech  43637  cantnfub2  43911  seff  44883  fargshiftf1  48045  fmtnoinf  48143  upgrimtrlslem2  48525  ushggricedg  48547  grtrimap  48568  oppff1o  49778  fucoppcid  50037  diag1f1o  50163  diag2f1o  50166