Theorem f1f 5393

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

Syntax hints:   → wi 4  ^◡ccnv 4603  Fun wfun 5182  ⟶wf 5184  –1-1→wf1 5185

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 5193

This theorem is referenced by:  f1rn  5394  f1fn  5395  f1ss  5399  f1ssres  5402  f1of  5432  dff1o5  5441  fsnd  5475  cocan1  5755  f1o2ndf1  6196  brdomg  6714  f1dom2g  6722  f1domg  6724  dom3d  6740  f1imaen2g  6759  2dom  6771  xpdom2  6797  dom0  6804  phplem4dom  6828  isinfinf  6863  infm  6870  updjudhcoinlf  7045  updjudhcoinrg  7046  casef1  7055  djudom  7058  difinfsnlem  7064  difinfsn  7065  fihashf1rn  10702  ennnfonelemrn  12352  reeff1o  13334  pwle2  13878