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  7038  f1dom2g  7048  f1domg  7050  dom3d  7066  f1imaen2g  7086  2dom  7099  1dom1el  7113  dom1o  7122  xpdom2  7135  dom0  7144  phplem4dom  7169  isinfinf  7207  infm  7217  f1setfi  7323  updjudhcoinlf  7427  updjudhcoinrg  7428  casef1  7437  djudom  7440  difinfsnlem  7446  difinfsn  7447  seqf1oglem1  10977  fihashf1rn  11249  hashf1lem1  11307  ennnfonelemrn  13368  reeff1o  16032  birthdaylem1g  16258  ushgruhgr  16559  umgr0e  16597  usgredgssen  16641  ausgrusgrben  16647  usgrss  16656  uspgrupgr  16660  usgrumgr  16663  usgrislfuspgrdom  16669  ushgredgedg  16705  ushgredgedgloop  16707  trlsegvdeglem6  16944  trlsegvdeglem7  16945  trlsegvdegfi  16946  eupth2lem3lem2fi  16948  eupth2lem3lem3fi  16949  eupth2lem3lem6fi  16950  eupth2lem3lem4fi  16952  3dom  17256  pwle2  17266