Theorem f1f 6724

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

Syntax hints:   → wi 4  ^◡ccnv 5622  Fun wfun 6480  ⟶wf 6482  –1-1→wf1 6483

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 6491

This theorem is referenced by:  f1fn  6725  f1ss  6729  f1ssres  6731  f1co  6735  f1of  6768  dff1o5  6777  f1un  6788  fsnd  6811  f1cofveqaeq  7198  f1cofveqaeqALT  7199  2f1fvneq  7201  f1dom3el3dif  7210  f1cdmsn  7223  f1prex  7225  cocan1  7232  fvf1pr  7248  f1iun  7886  f1dmex  7899  f1o2ndf1  8062  oacomf1olem  8489  brdomg  8891  f1dom2g  8902  f1domg  8904  dom3d  8926  f1imaen2g  8947  2dom  8962  domdifsn  8984  xpdom2  8996  domunsncan  9001  dom0  9029  fodomr  9052  domss2  9060  domssex2  9061  f1domfi  9105  sucdom2  9127  f1finf1o  9174  f1finf1oOLD  9175  infn0  9209  f1fi  9221  fodomfir  9237  oiexg  9446  hartogslem1  9453  infdifsn  9572  fseqenlem1  9937  fseqenlem2  9938  ac10ct  9947  acndom  9964  acndom2  9967  dfac12lem2  10058  dfac12lem3  10059  ackbij1  10150  fictb  10157  cfsmolem  10183  cfcoflem  10185  cfcof  10187  fin23lem17  10251  fin23lem32  10257  fin23lem39  10263  fin23lem41  10265  fin1a2lem6  10318  fin1a2lem7  10319  iundom2g  10453  alephreg  10495  canthnumlem  10561  canthwelem  10563  pwfseqlem1  10571  pwfseqlem5  10576  fvf1tp  13711  seqf1olem1  13966  hashf1rn  14277  hashimarn  14365  hashf1dmcdm  14369  hashf1lem1  14380  hashf1lem2  14381  cshf1  14734  setcmon  18012  injsubmefmnd  18789  odinf  19460  odcl2  19462  sylow1lem2  19496  gsumval3lem1  19802  gsumval3lem2  19803  gsumval3  19804  gsumzcl2  19807  gsumzf1o  19809  gsumzaddlem  19818  gsumzmhm  19834  gsumzoppg  19841  dprdf1  19932  f1lindf  21747  f1linds  21750  lindfmm  21752  mdetunilem8  22522  2ndcdisj  23359  itg1addlem4  25616  reeff1o  26373  birthdaylem1  26877  dchrisum0fno1  27438  ushgruhgr  29032  umgr0e  29073  usgredgss  29122  ausgrusgrb  29128  usgrss  29137  uspgrupgr  29141  usgrumgr  29144  usgruspgrb  29146  usgrislfuspgr  29150  usgredg2ALT  29156  ushgredgedg  29192  ushgredgedgloop  29194  usgr2pth  29727  0wlkons1  30083  trlsegvdeg  30189  fsumiunle  32787  cycpmco2lem1  33081  cycpmco2lem5  33085  cycpmco2  33088  cycpmconjv  33097  cyc3conja  33112  idomsubr  33261  islbs5  33330  qqhre  33989  esumiun  34063  erdszelem4  35169  erdszelem8  35173  erdszelem9  35174  erdsze2lem2  35179  pibt2  37393  aks6d1c2  42106  aks6d1c6lem3  42148  diophrw  42735  eldioph2lem2  42737  eldioph2  42738  eldioph2b  42739  dnwech  43024  cantnfub2  43298  seff  44285  fargshiftf1  47429  fmtnoinf  47524  upgrimtrlslem2  47893  ushggricedg  47915  grtrimap  47936  oppff1o  49138  fucoppcid  49397  diag1f1o  49523  diag2f1o  49526