Theorem f1f 5542

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

Syntax hints:   → wi 4  ^◡ccnv 4724  Fun wfun 5320  ⟶wf 5322  –1-1→wf1 5323

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 5331

This theorem is referenced by:  f1rn  5543  f1fn  5544  f1ss  5548  f1ssres  5551  f1of  5583  dff1o5  5592  fsnd  5628  cocan1  5928  f1o2ndf1  6393  brdomg  6919  f1dom2g  6929  f1domg  6931  dom3d  6947  f1imaen2g  6967  2dom  6980  1dom1el  6993  dom1o  7002  xpdom2  7015  dom0  7024  phplem4dom  7048  isinfinf  7086  infm  7096  updjudhcoinlf  7279  updjudhcoinrg  7280  casef1  7289  djudom  7292  difinfsnlem  7298  difinfsn  7299  seqf1oglem1  10782  fihashf1rn  11051  ennnfonelemrn  13045  reeff1o  15503  ushgruhgr  15937  umgr0e  15975  usgredgssen  16019  ausgrusgrben  16025  usgrss  16034  uspgrupgr  16038  usgrumgr  16041  usgrislfuspgrdom  16047  ushgredgedg  16083  ushgredgedgloop  16085  trlsegvdeglem6  16322  trlsegvdeglem7  16323  trlsegvdegfi  16324  eupth2lem3lem2fi  16326  eupth2lem3lem3fi  16327  eupth2lem3lem6fi  16328  eupth2lem3lem4fi  16330  3dom  16613  pwle2  16625