Theorem f1f 6730

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

Syntax hints:   → wi 4  ^◡ccnv 5623  Fun wfun 6486  ⟶wf 6488  –1-1→wf1 6489

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 6497

This theorem is referenced by:  f1fn  6731  f1ss  6735  f1ssres  6737  f1co  6741  f1of  6774  dff1o5  6783  f1un  6794  fsnd  6818  f1cofveqaeq  7203  f1cofveqaeqALT  7204  2f1fvneq  7206  f1dom3el3dif  7215  f1cdmsn  7228  f1prex  7230  cocan1  7237  fvf1pr  7253  f1iun  7888  f1dmex  7901  f1o2ndf1  8064  oacomf1olem  8491  brdomg  8895  f1dom2g  8906  f1domg  8908  dom3d  8931  f1imaen2g  8952  2dom  8967  domdifsn  8988  xpdom2  9000  domunsncan  9005  dom0  9033  fodomr  9056  domss2  9064  domssex2  9065  f1domfi  9105  sucdom2  9127  f1finf1o  9173  infn0  9202  f1fi  9214  fodomfir  9228  oiexg  9440  hartogslem1  9447  infdifsn  9566  fseqenlem1  9934  fseqenlem2  9935  ac10ct  9944  acndom  9961  acndom2  9964  dfac12lem2  10055  dfac12lem3  10056  ackbij1  10147  fictb  10154  cfsmolem  10180  cfcoflem  10182  cfcof  10184  fin23lem17  10248  fin23lem32  10254  fin23lem39  10260  fin23lem41  10262  fin1a2lem6  10315  fin1a2lem7  10316  iundom2g  10450  alephreg  10493  canthnumlem  10559  canthwelem  10561  pwfseqlem1  10569  pwfseqlem5  10574  fvf1tp  13709  seqf1olem1  13964  hashf1rn  14275  hashimarn  14363  hashf1dmcdm  14367  hashf1lem1  14378  hashf1lem2  14379  cshf1  14733  setcmon  18011  injsubmefmnd  18822  odinf  19492  odcl2  19494  sylow1lem2  19528  gsumval3lem1  19834  gsumval3lem2  19835  gsumval3  19836  gsumzcl2  19839  gsumzf1o  19841  gsumzaddlem  19850  gsumzmhm  19866  gsumzoppg  19873  dprdf1  19964  f1lindf  21777  f1linds  21780  lindfmm  21782  mdetunilem8  22563  2ndcdisj  23400  itg1addlem4  25656  reeff1o  26413  birthdaylem1  26917  dchrisum0fno1  27478  ushgruhgr  29142  umgr0e  29183  usgredgss  29232  ausgrusgrb  29238  usgrss  29247  uspgrupgr  29251  usgrumgr  29254  usgruspgrb  29256  usgrislfuspgr  29260  usgredg2ALT  29266  ushgredgedg  29302  ushgredgedgloop  29304  usgr2pth  29837  0wlkons1  30196  trlsegvdeg  30302  fsumiunle  32910  cycpmco2lem1  33208  cycpmco2lem5  33212  cycpmco2  33215  cycpmconjv  33224  cyc3conja  33239  idomsubr  33391  islbs5  33461  extdgfialglem1  33849  qqhre  34177  esumiun  34251  erdszelem4  35388  erdszelem8  35392  erdszelem9  35393  erdsze2lem2  35398  pibt2  37618  aks6d1c2  42380  aks6d1c6lem3  42422  diophrw  42997  eldioph2lem2  42999  eldioph2  43000  eldioph2b  43001  dnwech  43286  cantnfub2  43560  seff  44546  fargshiftf1  47683  fmtnoinf  47778  upgrimtrlslem2  48147  ushggricedg  48169  grtrimap  48190  oppff1o  49390  fucoppcid  49649  diag1f1o  49775  diag2f1o  49778