Theorem f1f 5598

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

This proof depends on syntax axioms:   → wi 4  ^◡ccnv 4773  Fun wfun 5371  ⟶wf 5373  –1-1→wf1 5374

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117  df-f1 5382

This theorem is used by:  f1rn  5599  f1fn  5600  f1ss  5604  f1ssres  5607  f1of  5639  dff1o5  5648  fsnd  5684  cocan1  5993  f1o2ndf1  6464  brdomg  7032  f1dom2g  7042  f1domg  7044  dom3d  7060  f1imaen2g  7080  2dom  7093  1dom1el  7107  dom1o  7116  xpdom2  7129  dom0  7138  phplem4dom  7163  isinfinf  7201  infm  7211  f1setfi  7317  updjudhcoinlf  7421  updjudhcoinrg  7422  casef1  7431  djudom  7434  difinfsnlem  7440  difinfsn  7441  seqf1oglem1  10970  fihashf1rn  11242  hashf1lem1  11300  ennnfonelemrn  13361  reeff1o  15926  birthdaylem1g  16147  ushgruhgr  16443  umgr0e  16481  usgredgssen  16525  ausgrusgrben  16531  usgrss  16540  uspgrupgr  16544  usgrumgr  16547  usgrislfuspgrdom  16553  ushgredgedg  16589  ushgredgedgloop  16591  trlsegvdeglem6  16828  trlsegvdeglem7  16829  trlsegvdegfi  16830  eupth2lem3lem2fi  16832  eupth2lem3lem3fi  16833  eupth2lem3lem6fi  16834  eupth2lem3lem4fi  16836  3dom  17140  pwle2  17150