Theorem f1f 5527

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

Syntax hints:   → wi 4  ^◡ccnv 4715  Fun wfun 5308  ⟶wf 5310  –1-1→wf1 5311

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 5319

This theorem is referenced by:  f1rn  5528  f1fn  5529  f1ss  5533  f1ssres  5536  f1of  5568  dff1o5  5577  fsnd  5612  cocan1  5904  f1o2ndf1  6364  brdomg  6887  f1dom2g  6897  f1domg  6899  dom3d  6915  f1imaen2g  6935  2dom  6948  xpdom2  6978  dom0  6987  phplem4dom  7011  isinfinf  7047  infm  7054  updjudhcoinlf  7235  updjudhcoinrg  7236  casef1  7245  djudom  7248  difinfsnlem  7254  difinfsn  7255  seqf1oglem1  10728  fihashf1rn  10997  ennnfonelemrn  12976  reeff1o  15432  ushgruhgr  15865  umgr0e  15903  usgredgssen  15945  ausgrusgrben  15951  usgrss  15960  uspgrupgr  15964  usgrumgr  15967  usgrislfuspgrdom  15973  ushgredgedg  16009  ushgredgedgloop  16011  1dom1el  16284  dom1o  16286  pwle2  16295