Theorem f1f 6759

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

Syntax hints:   → wi 4  ^◡ccnv 5640  Fun wfun 6508  ⟶wf 6510  –1-1→wf1 6511

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 6519

This theorem is referenced by:  f1fn  6760  f1ss  6764  f1ssres  6766  f1co  6770  f1of  6803  dff1o5  6812  f1un  6823  fsnd  6846  f1cofveqaeq  7235  f1cofveqaeqALT  7236  2f1fvneq  7238  f1dom3el3dif  7247  f1cdmsn  7260  f1prex  7262  cocan1  7269  fvf1pr  7285  f1iun  7925  f1dmex  7938  f1o2ndf1  8104  oacomf1olem  8531  brdomg  8933  f1dom2g  8944  f1domg  8946  dom3d  8968  f1imaen2g  8989  2dom  9004  domdifsn  9028  xpdom2  9041  domunsncan  9046  sucdom2OLD  9056  dom0  9075  fodomr  9098  domss2  9106  domssex2  9107  f1domfi  9151  sucdom2  9173  f1finf1o  9223  f1finf1oOLD  9224  infn0  9258  f1fi  9270  fodomfir  9286  oiexg  9495  hartogslem1  9502  infdifsn  9617  fseqenlem1  9984  fseqenlem2  9985  ac10ct  9994  acndom  10011  acndom2  10014  dfac12lem2  10105  dfac12lem3  10106  ackbij1  10197  fictb  10204  cfsmolem  10230  cfcoflem  10232  cfcof  10234  fin23lem17  10298  fin23lem32  10304  fin23lem39  10310  fin23lem41  10312  fin1a2lem6  10365  fin1a2lem7  10366  iundom2g  10500  alephreg  10542  canthnumlem  10608  canthwelem  10610  pwfseqlem1  10618  pwfseqlem5  10623  fvf1tp  13758  seqf1olem1  14013  hashf1rn  14324  hashimarn  14412  hashf1dmcdm  14416  hashf1lem1  14427  hashf1lem2  14428  cshf1  14782  setcmon  18056  injsubmefmnd  18831  odinf  19500  odcl2  19502  sylow1lem2  19536  gsumval3lem1  19842  gsumval3lem2  19843  gsumval3  19844  gsumzcl2  19847  gsumzf1o  19849  gsumzaddlem  19858  gsumzmhm  19874  gsumzoppg  19881  dprdf1  19972  f1lindf  21738  f1linds  21741  lindfmm  21743  mdetunilem8  22513  2ndcdisj  23350  itg1addlem4  25607  reeff1o  26364  birthdaylem1  26868  dchrisum0fno1  27429  ushgruhgr  29003  umgr0e  29044  usgredgss  29093  ausgrusgrb  29099  usgrss  29108  uspgrupgr  29112  usgrumgr  29115  usgruspgrb  29117  usgrislfuspgr  29121  usgredg2ALT  29127  ushgredgedg  29163  ushgredgedgloop  29165  usgr2pth  29701  0wlkons1  30057  trlsegvdeg  30163  fsumiunle  32761  cycpmco2lem1  33090  cycpmco2lem5  33094  cycpmco2  33097  cycpmconjv  33106  cyc3conja  33121  idomsubr  33266  islbs5  33358  qqhre  34017  esumiun  34091  erdszelem4  35188  erdszelem8  35192  erdszelem9  35193  erdsze2lem2  35198  pibt2  37412  aks6d1c2  42125  aks6d1c6lem3  42167  diophrw  42754  eldioph2lem2  42756  eldioph2  42757  eldioph2b  42758  dnwech  43044  cantnfub2  43318  seff  44305  fargshiftf1  47446  fmtnoinf  47541  upgrimtrlslem2  47909  ushggricedg  47931  grtrimap  47951  oppff1o  49142  fucoppcid  49401  diag1f1o  49527  diag2f1o  49530