Theorem f1f 6778

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

This proof depends on syntax axioms:   → wi 4  ^◡ccnv 5649  Fun wfun 6532  ⟶wf 6534  –1-1→wf1 6535

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 6543

This theorem is used by:  f1fn  6779  f1rel  6782  f1ss  6785  f1ssres  6787  f1co  6791  f1of  6824  dff1o5  6834  f1un  6845  fsnd  6869  f1cofveqaeq  7261  f1cofveqaeqALT  7262  2f1fvneq  7264  f1dom3el3dif  7273  f1cdmsn  7290  f1prex  7292  cocan1  7299  fvf1pr  7315  f1we  7363  f1iun  7956  f1dmex  7969  f1o2ndf1  8135  oacomf1olem  8575  brdomg  8988  f1dom2g  8999  f1domg  9001  dom3d  9024  f1imaen2g  9045  2dom  9061  domdifsn  9082  xpdom2  9094  domunsncan  9099  dom0  9127  fodomr  9150  domss2  9158  domssex2  9159  f1domfi  9199  sucdom2  9221  f1finf1o  9267  infn0  9297  f1fi  9309  fodomfir  9322  oiexg  9532  hartogslem1  9539  infdifsn  9661  fseqenlem1  10106  fseqenlem2  10107  acndom  10133  acndom2  10136  dfac12lem2  10226  dfac12lem3  10227  ackbij1  10318  fictb  10325  cfsmolem  10351  cfcoflem  10353  cfcof  10355  fin23lem17  10419  fin23lem32  10425  fin23lem39  10431  fin23lem41  10433  fin1a2lem6  10486  fin1a2lem7  10487  iundom2g  10627  alephreg  10670  canthnumlem  10736  canthwelem  10738  pwfseqlem1  10746  pwfseqlem5  10751  fvf1tp  13932  seqf1olem1  14187  hashf1rn  14499  hashimarn  14588  hashf1dmcdm  14592  hashf1lem1  14603  hashf1lem2  14604  cshf1  14965  setcmon  18267  injsubmefmnd  19098  odinf  19782  odcl2  19784  sylow1lem2  19818  gsumval3lem1  20124  gsumval3lem2  20125  gsumval3  20126  gsumzcl2  20129  gsumzf1o  20131  gsumzaddlem  20140  gsumzmhm  20156  gsumzoppg  20163  dprdf1  20254  f1lindf  22133  f1linds  22136  lindfmm  22138  mdetunilem8  22939  2ndcdisj  23780  itg1addlem4  26025  reeff1o  26779  birthdaylem1  27284  dchrisum0fno1  27843  ushgruhgr  29652  umgr0e  29693  usgredgss  29745  ausgrusgrb  29751  usgrss  29760  uspgrupgr  29764  usgrumgr  29767  usgruspgrb  29769  usgrislfuspgr  29773  usgredg2ALT  29779  ushgredgedg  29815  ushgredgedgloop  29817  usgr2pth  30355  0wlkons1  30717  trlsegvdeg  30833  fsumiunle  33466  cycpmco2lem1  33733  cycpmco2lem5  33737  cycpmco2  33740  cycpmconjv  33749  cyc3conja  33764  idomsubr  33917  islbs5  33981  extdgfialglem1  34370  qqhre  34698  esumiun  34772  omssubadd  34978  onf1we  35771  rncardr1prc  35814  vonf1wev  35955  vonf1onprcf1ac  35963  onprcf1acwevd  35966  prconf1acwevd  35967  erdszelem4  36045  erdszelem8  36049  erdszelem9  36050  erdsze2lem2  36055  mh-inf3f1  37421  pibt2  38433  aks6d1c2  43273  aks6d1c6lem3  43315  diophrw  43863  eldioph2lem2  43865  eldioph2  43866  eldioph2b  43867  cantnfub2  44417  seff  45386  fargshiftf1  48616  fmtnoinf  48714  upgrimtrlslem2  49096  ushggricedg  49118  grtrimap  49139  oppff1o  50358  fucoppcid  50636  diag1f1o  50762  diag2f1o  50768