Theorem f1f 5536

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

Syntax hints:   → wi 4  ^◡ccnv 4719  Fun wfun 5315  ⟶wf 5317  –1-1→wf1 5318

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 5326

This theorem is referenced by:  f1rn  5537  f1fn  5538  f1ss  5542  f1ssres  5545  f1of  5577  dff1o5  5586  fsnd  5621  cocan1  5920  f1o2ndf1  6385  brdomg  6910  f1dom2g  6920  f1domg  6922  dom3d  6938  f1imaen2g  6958  2dom  6971  dom1o  6990  xpdom2  7003  dom0  7012  phplem4dom  7036  isinfinf  7072  infm  7082  updjudhcoinlf  7263  updjudhcoinrg  7264  casef1  7273  djudom  7276  difinfsnlem  7282  difinfsn  7283  seqf1oglem1  10758  fihashf1rn  11027  ennnfonelemrn  13011  reeff1o  15468  ushgruhgr  15901  umgr0e  15939  usgredgssen  15981  ausgrusgrben  15987  usgrss  15996  uspgrupgr  16000  usgrumgr  16003  usgrislfuspgrdom  16009  ushgredgedg  16045  ushgredgedgloop  16047  1dom1el  16463  3dom  16465  pwle2  16477