Theorem f1f 5162

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

Syntax hints:   → wi 4  ^◡ccnv 4398  Fun wfun 4961  ⟶wf 4963  –1-1→wf1 4964

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 4972

This theorem is referenced by:  f1rn  5163  f1fn  5164  f1ss  5168  f1ssres  5171  f1of  5199  dff1o5  5208  cocan1  5504  f1o2ndf1  5926  brdomg  6393  f1dom2g  6401  f1domg  6403  dom3d  6419  f1imaen2g  6438  2dom  6450  xpdom2  6475  dom0  6482  phplem4dom  6506  isinfinf  6541  infm  6545  updjudhcoinlf  6676  updjudhcoinrg  6677  casef1  6686  djudom  6692  fihashf1rn  10030