Theorem f1f 5572

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

Syntax hints:   → wi 4  ^◡ccnv 4747  Fun wfun 5345  ⟶wf 5347  –1-1→wf1 5348

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 5356

This theorem is referenced by:  f1rn  5573  f1fn  5574  f1ss  5578  f1ssres  5581  f1of  5613  dff1o5  5622  fsnd  5658  cocan1  5959  f1o2ndf1  6423  brdomg  6984  f1dom2g  6994  f1domg  6996  dom3d  7012  f1imaen2g  7032  2dom  7045  1dom1el  7059  dom1o  7068  xpdom2  7081  dom0  7090  phplem4dom  7115  isinfinf  7153  infm  7163  updjudhcoinlf  7370  updjudhcoinrg  7371  casef1  7380  djudom  7383  difinfsnlem  7389  difinfsn  7390  seqf1oglem1  10880  fihashf1rn  11149  ennnfonelemrn  13162  reeff1o  15630  ushgruhgr  16067  umgr0e  16105  usgredgssen  16149  ausgrusgrben  16155  usgrss  16164  uspgrupgr  16168  usgrumgr  16171  usgrislfuspgrdom  16177  ushgredgedg  16213  ushgredgedgloop  16215  trlsegvdeglem6  16452  trlsegvdeglem7  16453  trlsegvdegfi  16454  eupth2lem3lem2fi  16456  eupth2lem3lem3fi  16457  eupth2lem3lem6fi  16458  eupth2lem3lem4fi  16460  3dom  16754  pwle2  16764