Theorem f1f 6756

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

Syntax hints:   → wi 4  ^◡ccnv 5637  Fun wfun 6505  ⟶wf 6507  –1-1→wf1 6508

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 6516

This theorem is referenced by:  f1fn  6757  f1ss  6761  f1ssres  6763  f1co  6767  f1of  6800  dff1o5  6809  f1un  6820  fsnd  6843  f1cofveqaeq  7232  f1cofveqaeqALT  7233  2f1fvneq  7235  f1dom3el3dif  7244  f1cdmsn  7257  f1prex  7259  cocan1  7266  fvf1pr  7282  f1iun  7922  f1dmex  7935  f1o2ndf1  8101  oacomf1olem  8528  brdomg  8930  f1dom2g  8941  f1domg  8943  dom3d  8965  f1imaen2g  8986  2dom  9001  domdifsn  9024  xpdom2  9036  domunsncan  9041  dom0  9069  fodomr  9092  domss2  9100  domssex2  9101  f1domfi  9145  sucdom2  9167  f1finf1o  9216  f1finf1oOLD  9217  infn0  9251  f1fi  9263  fodomfir  9279  oiexg  9488  hartogslem1  9495  infdifsn  9610  fseqenlem1  9977  fseqenlem2  9978  ac10ct  9987  acndom  10004  acndom2  10007  dfac12lem2  10098  dfac12lem3  10099  ackbij1  10190  fictb  10197  cfsmolem  10223  cfcoflem  10225  cfcof  10227  fin23lem17  10291  fin23lem32  10297  fin23lem39  10303  fin23lem41  10305  fin1a2lem6  10358  fin1a2lem7  10359  iundom2g  10493  alephreg  10535  canthnumlem  10601  canthwelem  10603  pwfseqlem1  10611  pwfseqlem5  10616  fvf1tp  13751  seqf1olem1  14006  hashf1rn  14317  hashimarn  14405  hashf1dmcdm  14409  hashf1lem1  14420  hashf1lem2  14421  cshf1  14775  setcmon  18049  injsubmefmnd  18824  odinf  19493  odcl2  19495  sylow1lem2  19529  gsumval3lem1  19835  gsumval3lem2  19836  gsumval3  19837  gsumzcl2  19840  gsumzf1o  19842  gsumzaddlem  19851  gsumzmhm  19867  gsumzoppg  19874  dprdf1  19965  f1lindf  21731  f1linds  21734  lindfmm  21736  mdetunilem8  22506  2ndcdisj  23343  itg1addlem4  25600  reeff1o  26357  birthdaylem1  26861  dchrisum0fno1  27422  ushgruhgr  28996  umgr0e  29037  usgredgss  29086  ausgrusgrb  29092  usgrss  29101  uspgrupgr  29105  usgrumgr  29108  usgruspgrb  29110  usgrislfuspgr  29114  usgredg2ALT  29120  ushgredgedg  29156  ushgredgedgloop  29158  usgr2pth  29694  0wlkons1  30050  trlsegvdeg  30156  fsumiunle  32754  cycpmco2lem1  33083  cycpmco2lem5  33087  cycpmco2  33090  cycpmconjv  33099  cyc3conja  33114  idomsubr  33259  islbs5  33351  qqhre  34010  esumiun  34084  erdszelem4  35181  erdszelem8  35185  erdszelem9  35186  erdsze2lem2  35191  pibt2  37405  aks6d1c2  42118  aks6d1c6lem3  42160  diophrw  42747  eldioph2lem2  42749  eldioph2  42750  eldioph2b  42751  dnwech  43037  cantnfub2  43311  seff  44298  fargshiftf1  47442  fmtnoinf  47537  upgrimtrlslem2  47905  ushggricedg  47927  grtrimap  47947  oppff1o  49138  fucoppcid  49397  diag1f1o  49523  diag2f1o  49526