Theorem f1f 5112

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

Syntax hints:   → wi 4  ^◡ccnv 4362  Fun wfun 4916  ⟶wf 4918  –1-1→wf1 4919

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

This theorem depends on definitions:  df-bi 115  df-f1 4927

This theorem is referenced by:  f1fn  5113  f1ss  5117  f1ssres  5119  f1of  5146  dff1o5  5155  fun11iun  5167  cocan1  5447  f1dmex  5763  f1o2ndf1  5869  brdomg  6252  f1dom2g  6259  f1domg  6261  dom3d  6277  f1imaen2g  6296  2dom  6308  xpdom2  6328  phplem4dom  6348