Theorem f1f 6398

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

Syntax hints:   → wi 4  ^◡ccnv 5399  Fun wfun 6176  ⟶wf 6178  –1-1→wf1 6179

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 199  df-an 388  df-f1 6187

This theorem is referenced by:  f1fn  6399  f1ss  6403  f1ssres  6405  f1of  6438  dff1o5  6447  fsnd  6480  f1cofveqaeq  6835  f1cofveqaeqALT  6836  2f1fvneq  6837  f1dom3el3dif  6846  f1prex  6859  cocan1  6866  fun11iun  7452  f1dmex  7464  f1o2ndf1  7616  oacomf1olem  7983  brdomg  8308  f1dom2g  8316  f1domg  8318  dom3d  8340  f1imaen2g  8359  2dom  8371  domdifsn  8388  xpdom2  8400  domunsncan  8405  fodomr  8456  domss2  8464  domssex2  8465  sucdom2  8501  f1finf1o  8532  f1fi  8598  oiexg  8786  hartogslem1  8793  infdifsn  8906  fseqenlem1  9236  fseqenlem2  9237  ac10ct  9246  acndom  9263  acndom2  9266  dfac12lem2  9356  dfac12lem3  9357  ackbij1  9450  fictb  9457  cfsmolem  9482  cfcoflem  9484  cfcof  9486  fin23lem17  9550  fin23lem32  9556  fin23lem39  9562  fin23lem41  9564  fin1a2lem6  9617  fin1a2lem7  9618  iundom2g  9752  alephreg  9794  canthnumlem  9860  canthwelem  9862  pwfseqlem1  9870  pwfseqlem5  9875  seqf1olem1  13217  hashf1rn  13521  hashimarn  13604  hashf1lem1  13616  hashf1lem2  13617  cshf1  14024  setcmon  17195  odinf  18441  odcl2  18443  sylow1lem2  18475  gsumval3lem1  18769  gsumval3lem2  18770  gsumval3  18771  gsumzcl2  18774  gsumzf1o  18776  gsumzaddlem  18784  gsumzmhm  18800  gsumzoppg  18807  dprdf1  18895  f1lindf  20658  f1linds  20661  lindfmm  20663  mdetunilem8  20922  2ndcdisj  21758  itg1addlem4  23993  reeff1o  24728  birthdaylem1  25221  dchrisum0fno1  25779  ushgruhgr  26547  umgr0e  26588  usgredgss  26637  ausgrusgrb  26643  usgrss  26652  uspgrupgr  26654  usgrumgr  26657  usgruspgrb  26659  usgrislfuspgr  26662  usgredg2ALT  26668  ushgredgedg  26704  ushgredgedgloop  26706  usgr2pth  27243  0wlkons1  27640  trlsegvdeg  27747  fsumiunle  30280  qqhre  30862  esumiun  30954  erdszelem4  31986  erdszelem8  31990  erdszelem9  31991  erdsze2lem2  31996  pibt2  34074  diophrw  38696  eldioph2lem2  38698  eldioph2  38699  eldioph2b  38700  dnwech  38989  seff  40001  fargshiftf1  42919  fmtnoinf  43006  ushrisomgr  43314