Theorem f1f 5463

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

Syntax hints:   → wi 4  ^◡ccnv 4662  Fun wfun 5252  ⟶wf 5254  –1-1→wf1 5255

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 5263

This theorem is referenced by:  f1rn  5464  f1fn  5465  f1ss  5469  f1ssres  5472  f1of  5504  dff1o5  5513  fsnd  5547  cocan1  5834  f1o2ndf1  6286  brdomg  6807  f1dom2g  6815  f1domg  6817  dom3d  6833  f1imaen2g  6852  2dom  6864  xpdom2  6890  dom0  6899  phplem4dom  6923  isinfinf  6958  infm  6965  updjudhcoinlf  7146  updjudhcoinrg  7147  casef1  7156  djudom  7159  difinfsnlem  7165  difinfsn  7166  seqf1oglem1  10611  fihashf1rn  10880  ennnfonelemrn  12636  reeff1o  15009  1dom1el  15637  pwle2  15643