Theorem f1f 5601

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

This proof depends on syntax axioms:   → wi 4  ^◡ccnv 4775  Fun wfun 5374  ⟶wf 5376  –1-1→wf1 5377

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 5385

This theorem is used by:  f1rn  5602  f1fn  5603  f1ss  5607  f1ssres  5610  f1of  5642  dff1o5  5651  fsnd  5687  cocan1  5996  f1o2ndf1  6468  brdomg  7037  f1dom2g  7047  f1domg  7049  dom3d  7065  f1imaen2g  7085  2dom  7098  1dom1el  7112  dom1o  7121  xpdom2  7134  dom0  7143  phplem4dom  7168  isinfinf  7206  infm  7216  f1setfi  7323  updjudhcoinlf  7427  updjudhcoinrg  7428  casef1  7437  djudom  7440  difinfsnlem  7446  difinfsn  7447  seqf1oglem1  10978  fihashf1rn  11250  hashf1lem1  11308  ennnfonelemrn  13369  reeff1o  16011  birthdaylem1g  16237  ushgruhgr  16538  umgr0e  16576  usgredgssen  16620  ausgrusgrben  16626  usgrss  16635  uspgrupgr  16639  usgrumgr  16642  usgrislfuspgrdom  16648  ushgredgedg  16684  ushgredgedgloop  16686  trlsegvdeglem6  16923  trlsegvdeglem7  16924  trlsegvdegfi  16925  eupth2lem3lem2fi  16927  eupth2lem3lem3fi  16928  eupth2lem3lem6fi  16929  eupth2lem3lem4fi  16931  3dom  17235  pwle2  17245