Theorem f1f 5578

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

Syntax hints:   → wi 4  ^◡ccnv 4753  Fun wfun 5351  ⟶wf 5353  –1-1→wf1 5354

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 5362

This theorem is referenced by:  f1rn  5579  f1fn  5580  f1ss  5584  f1ssres  5587  f1of  5619  dff1o5  5628  fsnd  5664  cocan1  5966  f1o2ndf1  6437  brdomg  6998  f1dom2g  7008  f1domg  7010  dom3d  7026  f1imaen2g  7046  2dom  7059  1dom1el  7073  dom1o  7082  xpdom2  7095  dom0  7104  phplem4dom  7129  isinfinf  7167  infm  7177  updjudhcoinlf  7384  updjudhcoinrg  7385  casef1  7394  djudom  7397  difinfsnlem  7403  difinfsn  7404  seqf1oglem1  10905  fihashf1rn  11176  ennnfonelemrn  13254  reeff1o  15750  ushgruhgr  16187  umgr0e  16225  usgredgssen  16269  ausgrusgrben  16275  usgrss  16284  uspgrupgr  16288  usgrumgr  16291  usgrislfuspgrdom  16297  ushgredgedg  16333  ushgredgedgloop  16335  trlsegvdeglem6  16572  trlsegvdeglem7  16573  trlsegvdegfi  16574  eupth2lem3lem2fi  16576  eupth2lem3lem3fi  16577  eupth2lem3lem6fi  16578  eupth2lem3lem4fi  16580  3dom  16874  pwle2  16884