Theorem f1f 6770

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

This proof depends on syntax axioms:   → wi 4  ^◡ccnv 5650  Fun wfun 6525  ⟶wf 6527  –1-1→wf1 6528

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 6536

This theorem is used by:  f1fn  6771  f1rel  6774  f1ss  6777  f1ssres  6779  f1co  6783  f1of  6816  dff1o5  6826  f1un  6837  fsnd  6861  f1cofveqaeq  7253  f1cofveqaeqALT  7254  2f1fvneq  7256  f1dom3el3dif  7265  f1cdmsn  7282  f1prex  7284  cocan1  7291  fvf1pr  7307  f1we  7355  f1iun  7945  f1dmex  7958  f1o2ndf1  8122  oacomf1olem  8556  brdomg  8969  f1dom2g  8980  f1domg  8982  dom3d  9005  f1imaen2g  9026  2dom  9042  domdifsn  9063  xpdom2  9075  domunsncan  9080  dom0  9108  fodomr  9131  domss2  9139  domssex2  9140  f1domfi  9180  sucdom2  9202  f1finf1o  9248  infn0  9278  f1fi  9290  fodomfir  9303  oiexg  9513  hartogslem1  9520  infdifsn  9642  fseqenlem1  10084  fseqenlem2  10085  acndom  10111  acndom2  10114  dfac12lem2  10204  dfac12lem3  10205  ackbij1  10296  fictb  10303  cfsmolem  10329  cfcoflem  10331  cfcof  10333  fin23lem17  10397  fin23lem32  10403  fin23lem39  10409  fin23lem41  10411  fin1a2lem6  10464  fin1a2lem7  10465  iundom2g  10605  alephreg  10648  canthnumlem  10714  canthwelem  10716  pwfseqlem1  10724  pwfseqlem5  10729  fvf1tp  13909  seqf1olem1  14164  hashf1rn  14476  hashimarn  14565  hashf1dmcdm  14569  hashf1lem1  14580  hashf1lem2  14581  cshf1  14941  setcmon  18242  injsubmefmnd  19073  odinf  19757  odcl2  19759  sylow1lem2  19793  gsumval3lem1  20099  gsumval3lem2  20100  gsumval3  20101  gsumzcl2  20104  gsumzf1o  20106  gsumzaddlem  20115  gsumzmhm  20131  gsumzoppg  20138  dprdf1  20229  f1lindf  22108  f1linds  22111  lindfmm  22113  mdetunilem8  22914  2ndcdisj  23755  itg1addlem4  26000  reeff1o  26756  birthdaylem1  27261  dchrisum0fno1  27820  ushgruhgr  29629  umgr0e  29670  usgredgss  29722  ausgrusgrb  29728  usgrss  29737  uspgrupgr  29741  usgrumgr  29744  usgruspgrb  29746  usgrislfuspgr  29750  usgredg2ALT  29756  ushgredgedg  29792  ushgredgedgloop  29794  usgr2pth  30332  0wlkons1  30694  trlsegvdeg  30810  fsumiunle  33402  cycpmco2lem1  33669  cycpmco2lem5  33673  cycpmco2  33676  cycpmconjv  33685  cyc3conja  33700  idomsubr  33853  islbs5  33917  extdgfialglem1  34306  qqhre  34634  esumiun  34708  vonf1wev  35860  erdszelem4  35928  erdszelem8  35932  erdszelem9  35933  erdsze2lem2  35938  mh-inf3f1  37299  pibt2  38308  aks6d1c2  43148  aks6d1c6lem3  43190  diophrw  43723  eldioph2lem2  43725  eldioph2  43726  eldioph2b  43727  cantnfub2  44282  seff  45252  fargshiftf1  48467  fmtnoinf  48565  upgrimtrlslem2  48947  ushggricedg  48969  grtrimap  48990  oppff1o  50201  fucoppcid  50460  diag1f1o  50586  diag2f1o  50589