Theorem f1f 5286

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

Syntax hints:   → wi 4  ^◡ccnv 4498  Fun wfun 5075  ⟶wf 5077  –1-1→wf1 5078

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116  df-f1 5086

This theorem is referenced by:  f1rn  5287  f1fn  5288  f1ss  5292  f1ssres  5295  f1of  5323  dff1o5  5332  cocan1  5642  f1o2ndf1  6079  brdomg  6596  f1dom2g  6604  f1domg  6606  dom3d  6622  f1imaen2g  6641  2dom  6653  xpdom2  6678  dom0  6685  phplem4dom  6709  isinfinf  6744  infm  6751  updjudhcoinlf  6917  updjudhcoinrg  6918  casef1  6927  djudom  6930  difinfsnlem  6936  difinfsn  6937  fihashf1rn  10428  ennnfonelemrn  11777  pwle2  12885