Theorem f1f 5387

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

Syntax hints:   → wi 4  ^◡ccnv 4597  Fun wfun 5176  ⟶wf 5178  –1-1→wf1 5179

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 5187

This theorem is referenced by:  f1rn  5388  f1fn  5389  f1ss  5393  f1ssres  5396  f1of  5426  dff1o5  5435  fsnd  5469  cocan1  5749  f1o2ndf1  6187  brdomg  6705  f1dom2g  6713  f1domg  6715  dom3d  6731  f1imaen2g  6750  2dom  6762  xpdom2  6788  dom0  6795  phplem4dom  6819  isinfinf  6854  infm  6861  updjudhcoinlf  7036  updjudhcoinrg  7037  casef1  7046  djudom  7049  difinfsnlem  7055  difinfsn  7056  fihashf1rn  10691  ennnfonelemrn  12289  reeff1o  13235  pwle2  13712