Theorem f1f 5328

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

Syntax hints:   → wi 4  ^◡ccnv 4538  Fun wfun 5117  ⟶wf 5119  –1-1→wf1 5120

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

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

This theorem is referenced by:  f1rn  5329  f1fn  5330  f1ss  5334  f1ssres  5337  f1of  5367  dff1o5  5376  fsnd  5410  cocan1  5688  f1o2ndf1  6125  brdomg  6642  f1dom2g  6650  f1domg  6652  dom3d  6668  f1imaen2g  6687  2dom  6699  xpdom2  6725  dom0  6732  phplem4dom  6756  isinfinf  6791  infm  6798  updjudhcoinlf  6965  updjudhcoinrg  6966  casef1  6975  djudom  6978  difinfsnlem  6984  difinfsn  6985  fihashf1rn  10535  ennnfonelemrn  11932  pwle2  13193