Theorem f1f 6800

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

This proof depends on syntax axioms:   → wi 4  ^◡ccnv 5654  Fun wfun 6552  ⟶wf 6554  ⟶1-1wf1 6555

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-f1 6563

This theorem is used by:  f1fn  6801  f1rel  6804  f1ss  6807  f1ssres  6809  f1co  6813  f1of  6846  dff1o5  6856  f1un  6867  fsnd  6892  f1cofveqaeq  7284  f1cofveqaeqALT  7285  2f1fvneq  7287  f1dom3el3dif  7296  f1cdmsn  7313  f1prex  7315  cocan1  7322  fvf1pr  7338  f1we  7386  f1iun  7980  f1dmex  7993  f1o2ndf1  8160  oacomf1olem  8600  brdomg  9013  f1dom2g  9024  f1domg  9026  dom3d  9049  f1imaen2g  9070  2dom  9086  domdifsn  9107  xpdom2  9119  domunsncan  9124  dom0  9152  fodomr  9175  domss2  9183  domssex2  9184  f1domfi  9224  sucdom2  9246  f1finf1o  9292  infn0  9322  f1fi  9334  fodomfir  9347  oiexg  9556  hartogslem1  9563  infdifsn  9685  fseqenlem1  10130  fseqenlem2  10131  acndom  10157  acndom2  10160  dfac12lem2  10250  dfac12lem3  10251  ackbij1  10342  fictb  10349  cfsmolem  10375  cfcoflem  10377  cfcof  10379  fin23lem17  10443  fin23lem32  10449  fin23lem39  10455  fin23lem41  10457  fin1a2lem6  10510  fin1a2lem7  10511  iundom2g  10651  alephreg  10694  canthnumlem  10760  canthwelem  10762  pwfseqlem1  10770  pwfseqlem5  10775  fvf1tp  13956  seqf1olem1  14211  hashf1rn  14523  hashimarn  14612  hashf1dmcdm  14616  hashf1lem1  14627  hashf1lem2  14628  cshf1  14989  setcmon  18291  injsubmefmnd  19122  odinf  19807  odcl2  19809  sylow1lem2  19843  gsumval3lem1  20149  gsumval3lem2  20150  gsumval3  20151  gsumzcl2  20154  gsumzf1o  20156  gsumzaddlem  20165  gsumzmhm  20181  gsumzoppg  20188  dprdf1  20279  f1lindf  22158  f1linds  22161  lindfmm  22163  mdetunilem8  22964  2ndcdisj  23805  itg1addlem4  26050  reeff1o  26804  birthdaylem1  27309  dchrisum0fno1  27868  ushgruhgr  29677  umgr0e  29718  usgredgss  29770  ausgrusgrb  29776  usgrss  29785  uspgrupgr  29789  usgrumgr  29792  usgruspgrb  29794  usgrislfuspgr  29798  usgredg2ALT  29804  ushgredgedg  29840  ushgredgedgloop  29842  usgr2pth  30380  0wlkons1  30742  trlsegvdeg  30858  fsumiunle  33490  cycpmco2lem1  33757  cycpmco2lem5  33761  cycpmco2  33764  cycpmconjv  33773  cyc3conja  33788  idomsubr  33941  islbs5  34005  extdgfialglem1  34394  qqhre  34722  esumiun  34796  omssubadd  35002  onf1we  35803  rncardr1prc  35850  jf1o  36011  jltaleph  36026  vonf1wev  36036  vonf1onprcf1ac  36044  onprcf1acwevd  36047  prconf1acwevd  36048  erdszelem4  36126  erdszelem8  36130  erdszelem9  36131  erdsze2lem2  36136  mh-inf3f1  37507  pibt2  38532  aks6d1c2  43372  aks6d1c6lem3  43414  diophrw  43963  eldioph2lem2  43965  eldioph2  43966  eldioph2b  43967  cantnfub2  44516  seff  45485  fargshiftf1  48728  fmtnoinf  48826  upgrimtrlslem2  49208  ushggricedg  49230  grtrimap  49251  oppff1o  50470  fucoppcid  50748  diag1f1o  50874  diag2f1o  50880