Theorem f1f 5596

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

Syntax hints:   → wi 4  ^◡ccnv 4771  Fun wfun 5369  ⟶wf 5371  –1-1→wf1 5372

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This theorem depends on definitions:  df-bi 117  df-f1 5380

This theorem is referenced by:  f1rn  5597  f1fn  5598  f1ss  5602  f1ssres  5605  f1of  5637  dff1o5  5646  fsnd  5682  cocan1  5987  f1o2ndf1  6458  brdomg  7026  f1dom2g  7036  f1domg  7038  dom3d  7054  f1imaen2g  7074  2dom  7087  1dom1el  7101  dom1o  7110  xpdom2  7123  dom0  7132  phplem4dom  7157  isinfinf  7195  infm  7205  f1setfi  7311  updjudhcoinlf  7414  updjudhcoinrg  7415  casef1  7424  djudom  7427  difinfsnlem  7433  difinfsn  7434  seqf1oglem1  10939  fihashf1rn  11210  hashf1lem1  11268  ennnfonelemrn  13293  reeff1o  15857  birthdaylem1g  16070  ushgruhgr  16304  umgr0e  16342  usgredgssen  16386  ausgrusgrben  16392  usgrss  16401  uspgrupgr  16405  usgrumgr  16408  usgrislfuspgrdom  16414  ushgredgedg  16450  ushgredgedgloop  16452  trlsegvdeglem6  16689  trlsegvdeglem7  16690  trlsegvdegfi  16691  eupth2lem3lem2fi  16693  eupth2lem3lem3fi  16694  eupth2lem3lem6fi  16695  eupth2lem3lem4fi  16697  3dom  17001  pwle2  17011