Theorem f1f 5459

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

Syntax hints:   → wi 4  ^◡ccnv 4658  Fun wfun 5248  ⟶wf 5250  –1-1→wf1 5251

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

This theorem depends on definitions:  df-bi 117  df-f1 5259

This theorem is referenced by:  f1rn  5460  f1fn  5461  f1ss  5465  f1ssres  5468  f1of  5500  dff1o5  5509  fsnd  5543  cocan1  5830  f1o2ndf1  6281  brdomg  6802  f1dom2g  6810  f1domg  6812  dom3d  6828  f1imaen2g  6847  2dom  6859  xpdom2  6885  dom0  6894  phplem4dom  6918  isinfinf  6953  infm  6960  updjudhcoinlf  7139  updjudhcoinrg  7140  casef1  7149  djudom  7152  difinfsnlem  7158  difinfsn  7159  seqf1oglem1  10590  fihashf1rn  10859  ennnfonelemrn  12576  reeff1o  14908  1dom1el  15483  pwle2  15489