Theorem f1f 5490

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

Syntax hints:   → wi 4  ^◡ccnv 4679  Fun wfun 5271  ⟶wf 5273  –1-1→wf1 5274

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 5282

This theorem is referenced by:  f1rn  5491  f1fn  5492  f1ss  5496  f1ssres  5499  f1of  5531  dff1o5  5540  fsnd  5575  cocan1  5866  f1o2ndf1  6324  brdomg  6847  f1dom2g  6857  f1domg  6859  dom3d  6875  f1imaen2g  6895  2dom  6908  xpdom2  6938  dom0  6947  phplem4dom  6971  isinfinf  7006  infm  7013  updjudhcoinlf  7194  updjudhcoinrg  7195  casef1  7204  djudom  7207  difinfsnlem  7213  difinfsn  7214  seqf1oglem1  10677  fihashf1rn  10946  ennnfonelemrn  12840  reeff1o  15295  ushgruhgr  15726  umgr0e  15761  1dom1el  16041  dom1o  16043  pwle2  16050