Theorem f1f 5200

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

Syntax hints:   → wi 4  ^◡ccnv 4427  Fun wfun 4996  ⟶wf 4998  –1-1→wf1 4999

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 5007

This theorem is referenced by:  f1rn  5201  f1fn  5202  f1ss  5206  f1ssres  5209  f1of  5237  dff1o5  5246  cocan1  5548  f1o2ndf1  5975  brdomg  6445  f1dom2g  6453  f1domg  6455  dom3d  6471  f1imaen2g  6490  2dom  6502  xpdom2  6527  dom0  6534  phplem4dom  6558  isinfinf  6593  infm  6600  updjudhcoinlf  6750  updjudhcoinrg  6751  casef1  6760  djudom  6766  fihashf1rn  10162