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 5618  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  6812  f1cofveqaeq  7197  f1cofveqaeqALT  7198  2f1fvneq  7200  f1dom3el3dif  7209  f1cdmsn  7222  f1prex  7224  cocan1  7231  fvf1pr  7247  f1iun  7882  f1dmex  7895  f1o2ndf1  8058  oacomf1olem  8485  brdomg  8887  f1dom2g  8898  f1domg  8900  dom3d  8923  f1imaen2g  8944  2dom  8959  domdifsn  8980  xpdom2  8992  domunsncan  8997  dom0  9025  fodomr  9048  domss2  9056  domssex2  9057  f1domfi  9097  sucdom2  9119  f1finf1o  9164  infn0  9193  f1fi  9205  fodomfir  9219  oiexg  9428  hartogslem1  9435  infdifsn  9554  fseqenlem1  9922  fseqenlem2  9923  ac10ct  9932  acndom  9949  acndom2  9952  dfac12lem2  10043  dfac12lem3  10044  ackbij1  10135  fictb  10142  cfsmolem  10168  cfcoflem  10170  cfcof  10172  fin23lem17  10236  fin23lem32  10242  fin23lem39  10248  fin23lem41  10250  fin1a2lem6  10303  fin1a2lem7  10304  iundom2g  10438  alephreg  10480  canthnumlem  10546  canthwelem  10548  pwfseqlem1  10556  pwfseqlem5  10561  fvf1tp  13695  seqf1olem1  13950  hashf1rn  14261  hashimarn  14349  hashf1dmcdm  14353  hashf1lem1  14364  hashf1lem2  14365  cshf1  14719  setcmon  17996  injsubmefmnd  18807  odinf  19477  odcl2  19479  sylow1lem2  19513  gsumval3lem1  19819  gsumval3lem2  19820  gsumval3  19821  gsumzcl2  19824  gsumzf1o  19826  gsumzaddlem  19835  gsumzmhm  19851  gsumzoppg  19858  dprdf1  19949  f1lindf  21761  f1linds  21764  lindfmm  21766  mdetunilem8  22535  2ndcdisj  23372  itg1addlem4  25628  reeff1o  26385  birthdaylem1  26889  dchrisum0fno1  27450  ushgruhgr  29049  umgr0e  29090  usgredgss  29139  ausgrusgrb  29145  usgrss  29154  uspgrupgr  29158  usgrumgr  29161  usgruspgrb  29163  usgrislfuspgr  29167  usgredg2ALT  29173  ushgredgedg  29209  ushgredgedgloop  29211  usgr2pth  29744  0wlkons1  30103  trlsegvdeg  30209  fsumiunle  32817  cycpmco2lem1  33102  cycpmco2lem5  33106  cycpmco2  33109  cycpmconjv  33118  cyc3conja  33133  idomsubr  33282  islbs5  33352  extdgfialglem1  33726  qqhre  34054  esumiun  34128  erdszelem4  35259  erdszelem8  35263  erdszelem9  35264  erdsze2lem2  35269  pibt2  37482  aks6d1c2  42244  aks6d1c6lem3  42286  diophrw  42877  eldioph2lem2  42879  eldioph2  42880  eldioph2b  42881  dnwech  43166  cantnfub2  43440  seff  44427  fargshiftf1  47566  fmtnoinf  47661  upgrimtrlslem2  48030  ushggricedg  48052  grtrimap  48073  oppff1o  49275  fucoppcid  49534  diag1f1o  49660  diag2f1o  49663