Theorem f1f 5092

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

Syntax hints:   → wi 4  ^◡ccnv 4344  Fun wfun 4896  ⟶wf 4898  –1-1→wf1 4899

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

This theorem depends on definitions:  df-bi 110  df-f1 4907

This theorem is referenced by:  f1fn  5093  f1ss  5097  f1ssres  5099  f1of  5126  dff1o5  5135  fun11iun  5147  cocan1  5427  f1dmex  5743  f1o2ndf1  5849  brdomg  6229  f1dom2g  6236  f1domg  6238  dom3d  6254  f1imaen2g  6273  2dom  6285  xpdom2  6305  phplem4dom  6324