Theorem f1f 5403

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

Syntax hints:   → wi 4  ^◡ccnv 4610  Fun wfun 5192  ⟶wf 5194  –1-1→wf1 5195

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 5203

This theorem is referenced by:  f1rn  5404  f1fn  5405  f1ss  5409  f1ssres  5412  f1of  5442  dff1o5  5451  fsnd  5485  cocan1  5766  f1o2ndf1  6207  brdomg  6726  f1dom2g  6734  f1domg  6736  dom3d  6752  f1imaen2g  6771  2dom  6783  xpdom2  6809  dom0  6816  phplem4dom  6840  isinfinf  6875  infm  6882  updjudhcoinlf  7057  updjudhcoinrg  7058  casef1  7067  djudom  7070  difinfsnlem  7076  difinfsn  7077  fihashf1rn  10723  ennnfonelemrn  12374  reeff1o  13488  pwle2  14031