Theorem f1f 6774

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 497	1 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵)

Syntax hints:   → wi 4  ^◡ccnv 5653  Fun wfun 6525  ⟶wf 6527  –1-1→wf1 6528

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 6536

This theorem is referenced by:  f1fn  6775  f1ss  6779  f1ssres  6781  f1co  6785  f1of  6818  dff1o5  6827  f1un  6838  fsnd  6861  f1cofveqaeq  7250  f1cofveqaeqALT  7251  2f1fvneq  7253  f1dom3el3dif  7262  f1cdmsn  7275  f1prex  7277  cocan1  7284  fvf1pr  7300  f1iun  7942  f1dmex  7955  f1o2ndf1  8121  oacomf1olem  8576  brdomg  8971  brdomgOLD  8972  f1dom2g  8984  f1domg  8986  dom3d  9008  f1imaen2g  9029  2dom  9044  domdifsn  9068  xpdom2  9081  domunsncan  9086  sucdom2OLD  9096  dom0  9116  fodomr  9142  domss2  9150  domssex2  9151  f1domfi  9195  sucdom2  9217  f1finf1o  9277  f1finf1oOLD  9278  infn0  9312  f1fi  9324  fodomfir  9340  oiexg  9549  hartogslem1  9556  infdifsn  9671  fseqenlem1  10038  fseqenlem2  10039  ac10ct  10048  acndom  10065  acndom2  10068  dfac12lem2  10159  dfac12lem3  10160  ackbij1  10251  fictb  10258  cfsmolem  10284  cfcoflem  10286  cfcof  10288  fin23lem17  10352  fin23lem32  10358  fin23lem39  10364  fin23lem41  10366  fin1a2lem6  10419  fin1a2lem7  10420  iundom2g  10554  alephreg  10596  canthnumlem  10662  canthwelem  10664  pwfseqlem1  10672  pwfseqlem5  10677  fvf1tp  13806  seqf1olem1  14059  hashf1rn  14370  hashimarn  14458  hashf1dmcdm  14462  hashf1lem1  14473  hashf1lem2  14474  cshf1  14828  setcmon  18100  injsubmefmnd  18875  odinf  19544  odcl2  19546  sylow1lem2  19580  gsumval3lem1  19886  gsumval3lem2  19887  gsumval3  19888  gsumzcl2  19891  gsumzf1o  19893  gsumzaddlem  19902  gsumzmhm  19918  gsumzoppg  19925  dprdf1  20016  f1lindf  21782  f1linds  21785  lindfmm  21787  mdetunilem8  22557  2ndcdisj  23394  itg1addlem4  25652  reeff1o  26409  birthdaylem1  26913  dchrisum0fno1  27474  ushgruhgr  29048  umgr0e  29089  usgredgss  29138  ausgrusgrb  29144  usgrss  29153  uspgrupgr  29157  usgrumgr  29160  usgruspgrb  29162  usgrislfuspgr  29166  usgredg2ALT  29172  ushgredgedg  29208  ushgredgedgloop  29210  usgr2pth  29746  0wlkons1  30102  trlsegvdeg  30208  fsumiunle  32808  cycpmco2lem1  33137  cycpmco2lem5  33141  cycpmco2  33144  cycpmconjv  33153  cyc3conja  33168  idomsubr  33303  islbs5  33395  qqhre  34051  esumiun  34125  erdszelem4  35216  erdszelem8  35220  erdszelem9  35221  erdsze2lem2  35226  pibt2  37435  aks6d1c2  42143  aks6d1c6lem3  42185  diophrw  42782  eldioph2lem2  42784  eldioph2  42785  eldioph2b  42786  dnwech  43072  cantnfub2  43346  seff  44333  fargshiftf1  47455  fmtnoinf  47550  upgrimtrlslem2  47918  ushggricedg  47940  grtrimap  47960  diag1f1o  49419  diag2f1o  49422