Theorem f1f 5551

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

Syntax hints:   → wi 4  ^◡ccnv 4730  Fun wfun 5327  ⟶wf 5329  –1-1→wf1 5330

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 5338

This theorem is referenced by:  f1rn  5552  f1fn  5553  f1ss  5557  f1ssres  5560  f1of  5592  dff1o5  5601  fsnd  5637  cocan1  5938  f1o2ndf1  6402  brdomg  6962  f1dom2g  6972  f1domg  6974  dom3d  6990  f1imaen2g  7010  2dom  7023  1dom1el  7036  dom1o  7045  xpdom2  7058  dom0  7067  phplem4dom  7091  isinfinf  7129  infm  7139  updjudhcoinlf  7322  updjudhcoinrg  7323  casef1  7332  djudom  7335  difinfsnlem  7341  difinfsn  7342  seqf1oglem1  10825  fihashf1rn  11094  ennnfonelemrn  13101  reeff1o  15564  ushgruhgr  16001  umgr0e  16039  usgredgssen  16083  ausgrusgrben  16089  usgrss  16098  uspgrupgr  16102  usgrumgr  16105  usgrislfuspgrdom  16111  ushgredgedg  16147  ushgredgedgloop  16149  trlsegvdeglem6  16386  trlsegvdeglem7  16387  trlsegvdegfi  16388  eupth2lem3lem2fi  16390  eupth2lem3lem3fi  16391  eupth2lem3lem6fi  16392  eupth2lem3lem4fi  16394  3dom  16688  pwle2  16700