Theorem f1f 5539

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

Syntax hints:   → wi 4  ^◡ccnv 4722  Fun wfun 5318  ⟶wf 5320  –1-1→wf1 5321

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 5329

This theorem is referenced by:  f1rn  5540  f1fn  5541  f1ss  5545  f1ssres  5548  f1of  5580  dff1o5  5589  fsnd  5624  cocan1  5923  f1o2ndf1  6388  brdomg  6914  f1dom2g  6924  f1domg  6926  dom3d  6942  f1imaen2g  6962  2dom  6975  1dom1el  6988  dom1o  6997  xpdom2  7010  dom0  7019  phplem4dom  7043  isinfinf  7081  infm  7091  updjudhcoinlf  7273  updjudhcoinrg  7274  casef1  7283  djudom  7286  difinfsnlem  7292  difinfsn  7293  seqf1oglem1  10774  fihashf1rn  11043  ennnfonelemrn  13033  reeff1o  15490  ushgruhgr  15924  umgr0e  15962  usgredgssen  16006  ausgrusgrben  16012  usgrss  16021  uspgrupgr  16025  usgrumgr  16028  usgrislfuspgrdom  16034  ushgredgedg  16070  ushgredgedgloop  16072  3dom  16537  pwle2  16549