Theorem f1f 5460

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

Syntax hints:   → wi 4  ^◡ccnv 4659  Fun wfun 5249  ⟶wf 5251  –1-1→wf1 5252

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 5260

This theorem is referenced by:  f1rn  5461  f1fn  5462  f1ss  5466  f1ssres  5469  f1of  5501  dff1o5  5510  fsnd  5544  cocan1  5831  f1o2ndf1  6283  brdomg  6804  f1dom2g  6812  f1domg  6814  dom3d  6830  f1imaen2g  6849  2dom  6861  xpdom2  6887  dom0  6896  phplem4dom  6920  isinfinf  6955  infm  6962  updjudhcoinlf  7141  updjudhcoinrg  7142  casef1  7151  djudom  7154  difinfsnlem  7160  difinfsn  7161  seqf1oglem1  10593  fihashf1rn  10862  ennnfonelemrn  12579  reeff1o  14949  1dom1el  15553  pwle2  15559