Theorem f1f 5533

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

Syntax hints:   → wi 4  ^◡ccnv 4718  Fun wfun 5312  ⟶wf 5314  –1-1→wf1 5315

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 5323

This theorem is referenced by:  f1rn  5534  f1fn  5535  f1ss  5539  f1ssres  5542  f1of  5574  dff1o5  5583  fsnd  5618  cocan1  5917  f1o2ndf1  6380  brdomg  6905  f1dom2g  6915  f1domg  6917  dom3d  6933  f1imaen2g  6953  2dom  6966  dom1o  6985  xpdom2  6998  dom0  7007  phplem4dom  7031  isinfinf  7067  infm  7074  updjudhcoinlf  7255  updjudhcoinrg  7256  casef1  7265  djudom  7268  difinfsnlem  7274  difinfsn  7275  seqf1oglem1  10749  fihashf1rn  11018  ennnfonelemrn  12998  reeff1o  15455  ushgruhgr  15888  umgr0e  15926  usgredgssen  15968  ausgrusgrben  15974  usgrss  15983  uspgrupgr  15987  usgrumgr  15990  usgrislfuspgrdom  15996  ushgredgedg  16032  ushgredgedgloop  16034  1dom1el  16378  3dom  16381  pwle2  16393