Theorem f1f 6788

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

Syntax hints:   → wi 4  ^◡ccnv 5676  Fun wfun 6538  ⟶wf 6540  –1-1→wf1 6541

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 398  df-f1 6549

This theorem is referenced by:  f1fn  6789  f1ss  6794  f1ssres  6796  f1co  6800  f1of  6834  dff1o5  6843  f1un  6854  fsnd  6877  f1cofveqaeq  7257  f1cofveqaeqALT  7258  2f1fvneq  7259  f1dom3el3dif  7268  f1cdmsn  7280  f1prex  7282  cocan1  7289  f1iun  7930  f1dmex  7943  f1o2ndf1  8108  oacomf1olem  8564  brdomg  8952  brdomgOLD  8953  f1dom2g  8965  f1dom2gOLD  8966  f1domg  8968  dom3d  8990  f1imaen2g  9011  2dom  9030  domdifsn  9054  xpdom2  9067  domunsncan  9072  sucdom2OLD  9082  dom0  9102  fodomr  9128  domss2  9136  domssex2  9137  f1domfi  9184  sucdom2  9206  f1finf1o  9271  f1finf1oOLD  9272  infn0  9307  f1fi  9339  oiexg  9530  hartogslem1  9537  infdifsn  9652  fseqenlem1  10019  fseqenlem2  10020  ac10ct  10029  acndom  10046  acndom2  10049  dfac12lem2  10139  dfac12lem3  10140  ackbij1  10233  fictb  10240  cfsmolem  10265  cfcoflem  10267  cfcof  10269  fin23lem17  10333  fin23lem32  10339  fin23lem39  10345  fin23lem41  10347  fin1a2lem6  10400  fin1a2lem7  10401  iundom2g  10535  alephreg  10577  canthnumlem  10643  canthwelem  10645  pwfseqlem1  10653  pwfseqlem5  10658  seqf1olem1  14007  hashf1rn  14312  hashimarn  14400  hashf1lem1  14415  hashf1lem1OLD  14416  hashf1lem2  14417  cshf1  14760  setcmon  18037  injsubmefmnd  18778  odinf  19431  odcl2  19433  sylow1lem2  19467  gsumval3lem1  19773  gsumval3lem2  19774  gsumval3  19775  gsumzcl2  19778  gsumzf1o  19780  gsumzaddlem  19789  gsumzmhm  19805  gsumzoppg  19812  dprdf1  19903  f1lindf  21377  f1linds  21380  lindfmm  21382  mdetunilem8  22121  2ndcdisj  22960  itg1addlem4  25216  itg1addlem4OLD  25217  reeff1o  25959  birthdaylem1  26456  dchrisum0fno1  27014  ushgruhgr  28329  umgr0e  28370  usgredgss  28419  ausgrusgrb  28425  usgrss  28434  uspgrupgr  28436  usgrumgr  28439  usgruspgrb  28441  usgrislfuspgr  28444  usgredg2ALT  28450  ushgredgedg  28486  ushgredgedgloop  28488  usgr2pth  29021  0wlkons1  29374  trlsegvdeg  29480  fsumiunle  32035  cycpmco2lem1  32285  cycpmco2lem5  32289  cycpmco2  32292  cycpmconjv  32301  cyc3conja  32316  islbs5  32496  qqhre  33000  esumiun  33092  hashf1dmcdm  34105  erdszelem4  34185  erdszelem8  34189  erdszelem9  34190  erdsze2lem2  34195  pibt2  36298  diophrw  41497  eldioph2lem2  41499  eldioph2  41500  eldioph2b  41501  dnwech  41790  cantnfub2  42072  seff  43068  fargshiftf1  46109  fmtnoinf  46204  ushrisomgr  46509