Theorem f1f 6817

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

Syntax hints:   → wi 4  ^◡ccnv 5699  Fun wfun 6567  ⟶wf 6569  –1-1→wf1 6570

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 6578

This theorem is referenced by:  f1fn  6818  f1ss  6822  f1ssres  6824  f1co  6828  f1of  6862  dff1o5  6871  f1un  6882  fsnd  6905  f1cofveqaeq  7295  f1cofveqaeqALT  7296  2f1fvneq  7297  f1dom3el3dif  7306  f1cdmsn  7318  f1prex  7320  cocan1  7327  fvf1pr  7343  f1iun  7984  f1dmex  7997  f1o2ndf1  8163  oacomf1olem  8620  brdomg  9016  brdomgOLD  9017  f1dom2g  9029  f1dom2gOLD  9030  f1domg  9032  dom3d  9054  f1imaen2g  9075  2dom  9095  domdifsn  9120  xpdom2  9133  domunsncan  9138  sucdom2OLD  9148  dom0  9168  fodomr  9194  domss2  9202  domssex2  9203  f1domfi  9247  sucdom2  9269  f1finf1o  9333  f1finf1oOLD  9334  infn0  9368  f1fi  9380  fodomfir  9396  oiexg  9604  hartogslem1  9611  infdifsn  9726  fseqenlem1  10093  fseqenlem2  10094  ac10ct  10103  acndom  10120  acndom2  10123  dfac12lem2  10214  dfac12lem3  10215  ackbij1  10306  fictb  10313  cfsmolem  10339  cfcoflem  10341  cfcof  10343  fin23lem17  10407  fin23lem32  10413  fin23lem39  10419  fin23lem41  10421  fin1a2lem6  10474  fin1a2lem7  10475  iundom2g  10609  alephreg  10651  canthnumlem  10717  canthwelem  10719  pwfseqlem1  10727  pwfseqlem5  10732  fvf1tp  13840  seqf1olem1  14092  hashf1rn  14401  hashimarn  14489  hashf1dmcdm  14493  hashf1lem1  14504  hashf1lem2  14505  cshf1  14858  setcmon  18154  injsubmefmnd  18932  odinf  19605  odcl2  19607  sylow1lem2  19641  gsumval3lem1  19947  gsumval3lem2  19948  gsumval3  19949  gsumzcl2  19952  gsumzf1o  19954  gsumzaddlem  19963  gsumzmhm  19979  gsumzoppg  19986  dprdf1  20077  f1lindf  21865  f1linds  21868  lindfmm  21870  mdetunilem8  22646  2ndcdisj  23485  itg1addlem4  25753  itg1addlem4OLD  25754  reeff1o  26509  birthdaylem1  27012  dchrisum0fno1  27573  ushgruhgr  29104  umgr0e  29145  usgredgss  29194  ausgrusgrb  29200  usgrss  29209  uspgrupgr  29213  usgrumgr  29216  usgruspgrb  29218  usgrislfuspgr  29222  usgredg2ALT  29228  ushgredgedg  29264  ushgredgedgloop  29266  usgr2pth  29800  0wlkons1  30153  trlsegvdeg  30259  fsumiunle  32833  cycpmco2lem1  33119  cycpmco2lem5  33123  cycpmco2  33126  cycpmconjv  33135  cyc3conja  33150  idomsubr  33276  islbs5  33373  qqhre  33966  esumiun  34058  erdszelem4  35162  erdszelem8  35166  erdszelem9  35167  erdsze2lem2  35172  pibt2  37383  aks6d1c2  42087  aks6d1c6lem3  42129  diophrw  42715  eldioph2lem2  42717  eldioph2  42718  eldioph2b  42719  dnwech  43005  cantnfub2  43284  seff  44278  fargshiftf1  47315  fmtnoinf  47410  ushggricedg  47780  grtrimap  47797