Theorem f1f 6679

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

Syntax hints:   → wi 4  ^◡ccnv 5589  Fun wfun 6431  ⟶wf 6433  –1-1→wf1 6434

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 206  df-an 397  df-f1 6442

This theorem is referenced by:  f1fn  6680  f1ss  6685  f1ssres  6687  f1co  6691  f1of  6725  dff1o5  6734  f1un  6745  fsnd  6768  f1cofveqaeq  7140  f1cofveqaeqALT  7141  2f1fvneq  7142  f1dom3el3dif  7151  f1cdmsn  7163  f1prex  7165  cocan1  7172  f1iun  7795  f1dmex  7808  f1o2ndf1  7972  oacomf1olem  8404  brdomg  8755  brdomgOLD  8756  f1dom2g  8766  f1dom2gOLD  8767  f1domg  8769  dom3d  8791  f1imaen2g  8810  2dom  8829  domdifsn  8850  xpdom2  8863  domunsncan  8868  sucdom2OLD  8878  dom0  8898  fodomr  8924  domss2  8932  domssex2  8933  f1domfi  8976  sucdom2  8998  f1finf1o  9055  f1fi  9115  oiexg  9303  hartogslem1  9310  infdifsn  9424  fseqenlem1  9789  fseqenlem2  9790  ac10ct  9799  acndom  9816  acndom2  9819  dfac12lem2  9909  dfac12lem3  9910  ackbij1  10003  fictb  10010  cfsmolem  10035  cfcoflem  10037  cfcof  10039  fin23lem17  10103  fin23lem32  10109  fin23lem39  10115  fin23lem41  10117  fin1a2lem6  10170  fin1a2lem7  10171  iundom2g  10305  alephreg  10347  canthnumlem  10413  canthwelem  10415  pwfseqlem1  10423  pwfseqlem5  10428  seqf1olem1  13771  hashf1rn  14076  hashimarn  14164  hashf1lem1  14177  hashf1lem1OLD  14178  hashf1lem2  14179  cshf1  14532  setcmon  17811  injsubmefmnd  18545  odinf  19179  odcl2  19181  sylow1lem2  19213  gsumval3lem1  19515  gsumval3lem2  19516  gsumval3  19517  gsumzcl2  19520  gsumzf1o  19522  gsumzaddlem  19531  gsumzmhm  19547  gsumzoppg  19554  dprdf1  19645  f1lindf  21038  f1linds  21041  lindfmm  21043  mdetunilem8  21777  2ndcdisj  22616  itg1addlem4  24872  itg1addlem4OLD  24873  reeff1o  25615  birthdaylem1  26110  dchrisum0fno1  26668  ushgruhgr  27448  umgr0e  27489  usgredgss  27538  ausgrusgrb  27544  usgrss  27553  uspgrupgr  27555  usgrumgr  27558  usgruspgrb  27560  usgrislfuspgr  27563  usgredg2ALT  27569  ushgredgedg  27605  ushgredgedgloop  27607  usgr2pth  28141  0wlkons1  28494  trlsegvdeg  28600  fsumiunle  31152  cycpmco2lem1  31402  cycpmco2lem5  31406  cycpmco2  31409  cycpmconjv  31418  cyc3conja  31433  qqhre  31979  esumiun  32071  hashf1dmcdm  33085  erdszelem4  33165  erdszelem8  33169  erdszelem9  33170  erdsze2lem2  33175  pibt2  35597  diophrw  40588  eldioph2lem2  40590  eldioph2  40591  eldioph2b  40592  dnwech  40880  seff  41934  fargshiftf1  44904  fmtnoinf  44999  ushrisomgr  45304