Theorem f1f 6804

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

Syntax hints:   → wi 4  ^◡ccnv 5687  Fun wfun 6556  ⟶wf 6558  –1-1→wf1 6559

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 6567

This theorem is referenced by:  f1fn  6805  f1ss  6809  f1ssres  6811  f1co  6815  f1of  6848  dff1o5  6857  f1un  6868  fsnd  6891  f1cofveqaeq  7277  f1cofveqaeqALT  7278  2f1fvneq  7279  f1dom3el3dif  7288  f1cdmsn  7301  f1prex  7303  cocan1  7310  fvf1pr  7326  f1iun  7966  f1dmex  7979  f1o2ndf1  8145  oacomf1olem  8600  brdomg  8995  brdomgOLD  8996  f1dom2g  9008  f1domg  9010  dom3d  9032  f1imaen2g  9053  2dom  9068  domdifsn  9092  xpdom2  9105  domunsncan  9110  sucdom2OLD  9120  dom0  9140  fodomr  9166  domss2  9174  domssex2  9175  f1domfi  9218  sucdom2  9240  f1finf1o  9302  f1finf1oOLD  9303  infn0  9337  f1fi  9349  fodomfir  9365  oiexg  9572  hartogslem1  9579  infdifsn  9694  fseqenlem1  10061  fseqenlem2  10062  ac10ct  10071  acndom  10088  acndom2  10091  dfac12lem2  10182  dfac12lem3  10183  ackbij1  10274  fictb  10281  cfsmolem  10307  cfcoflem  10309  cfcof  10311  fin23lem17  10375  fin23lem32  10381  fin23lem39  10387  fin23lem41  10389  fin1a2lem6  10442  fin1a2lem7  10443  iundom2g  10577  alephreg  10619  canthnumlem  10685  canthwelem  10687  pwfseqlem1  10695  pwfseqlem5  10700  fvf1tp  13825  seqf1olem1  14078  hashf1rn  14387  hashimarn  14475  hashf1dmcdm  14479  hashf1lem1  14490  hashf1lem2  14491  cshf1  14844  setcmon  18140  injsubmefmnd  18922  odinf  19595  odcl2  19597  sylow1lem2  19631  gsumval3lem1  19937  gsumval3lem2  19938  gsumval3  19939  gsumzcl2  19942  gsumzf1o  19944  gsumzaddlem  19953  gsumzmhm  19969  gsumzoppg  19976  dprdf1  20067  f1lindf  21859  f1linds  21862  lindfmm  21864  mdetunilem8  22640  2ndcdisj  23479  itg1addlem4  25747  itg1addlem4OLD  25748  reeff1o  26505  birthdaylem1  27008  dchrisum0fno1  27569  ushgruhgr  29100  umgr0e  29141  usgredgss  29190  ausgrusgrb  29196  usgrss  29205  uspgrupgr  29209  usgrumgr  29212  usgruspgrb  29214  usgrislfuspgr  29218  usgredg2ALT  29224  ushgredgedg  29260  ushgredgedgloop  29262  usgr2pth  29796  0wlkons1  30149  trlsegvdeg  30255  fsumiunle  32835  cycpmco2lem1  33128  cycpmco2lem5  33132  cycpmco2  33135  cycpmconjv  33144  cyc3conja  33159  idomsubr  33290  islbs5  33387  qqhre  33982  esumiun  34074  erdszelem4  35178  erdszelem8  35182  erdszelem9  35183  erdsze2lem2  35188  pibt2  37399  aks6d1c2  42111  aks6d1c6lem3  42153  diophrw  42746  eldioph2lem2  42748  eldioph2  42749  eldioph2b  42750  dnwech  43036  cantnfub2  43311  seff  44304  fargshiftf1  47365  fmtnoinf  47460  ushggricedg  47833  grtrimap  47850