Theorem f1f 6785

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

Syntax hints:   → wi 4  ^◡ccnv 5675  Fun wfun 6535  ⟶wf 6537  –1-1→wf1 6538

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 6546

This theorem is referenced by:  f1fn  6786  f1ss  6791  f1ssres  6793  f1co  6797  f1of  6831  dff1o5  6840  f1un  6851  fsnd  6874  f1cofveqaeq  7254  f1cofveqaeqALT  7255  2f1fvneq  7256  f1dom3el3dif  7265  f1cdmsn  7277  f1prex  7279  cocan1  7286  f1iun  7927  f1dmex  7940  f1o2ndf1  8105  oacomf1olem  8561  brdomg  8949  brdomgOLD  8950  f1dom2g  8962  f1dom2gOLD  8963  f1domg  8965  dom3d  8987  f1imaen2g  9008  2dom  9027  domdifsn  9051  xpdom2  9064  domunsncan  9069  sucdom2OLD  9079  dom0  9099  fodomr  9125  domss2  9133  domssex2  9134  f1domfi  9181  sucdom2  9203  f1finf1o  9268  f1finf1oOLD  9269  infn0  9304  f1fi  9336  oiexg  9527  hartogslem1  9534  infdifsn  9649  fseqenlem1  10016  fseqenlem2  10017  ac10ct  10026  acndom  10043  acndom2  10046  dfac12lem2  10136  dfac12lem3  10137  ackbij1  10230  fictb  10237  cfsmolem  10262  cfcoflem  10264  cfcof  10266  fin23lem17  10330  fin23lem32  10336  fin23lem39  10342  fin23lem41  10344  fin1a2lem6  10397  fin1a2lem7  10398  iundom2g  10532  alephreg  10574  canthnumlem  10640  canthwelem  10642  pwfseqlem1  10650  pwfseqlem5  10655  seqf1olem1  14004  hashf1rn  14309  hashimarn  14397  hashf1lem1  14412  hashf1lem1OLD  14413  hashf1lem2  14414  cshf1  14757  setcmon  18034  injsubmefmnd  18775  odinf  19426  odcl2  19428  sylow1lem2  19462  gsumval3lem1  19768  gsumval3lem2  19769  gsumval3  19770  gsumzcl2  19773  gsumzf1o  19775  gsumzaddlem  19784  gsumzmhm  19800  gsumzoppg  19807  dprdf1  19898  f1lindf  21369  f1linds  21372  lindfmm  21374  mdetunilem8  22113  2ndcdisj  22952  itg1addlem4  25208  itg1addlem4OLD  25209  reeff1o  25951  birthdaylem1  26446  dchrisum0fno1  27004  ushgruhgr  28319  umgr0e  28360  usgredgss  28409  ausgrusgrb  28415  usgrss  28424  uspgrupgr  28426  usgrumgr  28429  usgruspgrb  28431  usgrislfuspgr  28434  usgredg2ALT  28440  ushgredgedg  28476  ushgredgedgloop  28478  usgr2pth  29011  0wlkons1  29364  trlsegvdeg  29470  fsumiunle  32023  cycpmco2lem1  32273  cycpmco2lem5  32277  cycpmco2  32280  cycpmconjv  32289  cyc3conja  32304  islbs5  32485  qqhre  32989  esumiun  33081  hashf1dmcdm  34094  erdszelem4  34174  erdszelem8  34178  erdszelem9  34179  erdsze2lem2  34184  pibt2  36287  diophrw  41483  eldioph2lem2  41485  eldioph2  41486  eldioph2b  41487  dnwech  41776  cantnfub2  42058  seff  43054  fargshiftf1  46096  fmtnoinf  46191  ushrisomgr  46496