Theorem f1f 5598

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

This proof depends on syntax axioms:   → wi 4  ^◡ccnv 4773  Fun wfun 5371  ⟶wf 5373  –1-1→wf1 5374

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117  df-f1 5382

This theorem is used by:  f1rn  5599  f1fn  5600  f1ss  5604  f1ssres  5607  f1of  5639  dff1o5  5648  fsnd  5684  cocan1  5993  f1o2ndf1  6464  brdomg  7032  f1dom2g  7042  f1domg  7044  dom3d  7060  f1imaen2g  7080  2dom  7093  1dom1el  7107  dom1o  7116  xpdom2  7129  dom0  7138  phplem4dom  7163  isinfinf  7201  infm  7211  f1setfi  7317  updjudhcoinlf  7420  updjudhcoinrg  7421  casef1  7430  djudom  7433  difinfsnlem  7439  difinfsn  7440  seqf1oglem1  10958  fihashf1rn  11229  hashf1lem1  11287  ennnfonelemrn  13312  reeff1o  15876  birthdaylem1g  16093  ushgruhgr  16333  umgr0e  16371  usgredgssen  16415  ausgrusgrben  16421  usgrss  16430  uspgrupgr  16434  usgrumgr  16437  usgrislfuspgrdom  16443  ushgredgedg  16479  ushgredgedgloop  16481  trlsegvdeglem6  16718  trlsegvdeglem7  16719  trlsegvdegfi  16720  eupth2lem3lem2fi  16722  eupth2lem3lem3fi  16723  eupth2lem3lem6fi  16724  eupth2lem3lem4fi  16726  3dom  17030  pwle2  17040