Theorem f1of1 5366

Description: A one-to-one onto mapping is a one-to-one mapping. (Contributed by NM, 12-Dec-2003.)

Assertion

Ref	Expression
f1of1	⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴–1-1→𝐵)

Proof of Theorem f1of1

Step	Hyp	Ref	Expression
1		df-f1o 5130	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))
2	1	simplbi 272	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴–1-1→𝐵)

Syntax hints:   → wi 4  –1-1→wf1 5120  –onto→wfo 5121  –1-1-onto→wf1o 5122

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116  df-f1o 5130

This theorem is referenced by:  f1of  5367  f1sng  5409  f1oresrab  5585  f1ocnvfvrneq  5683  isores3  5716  isoini2  5720  f1oiso  5727  f1opw2  5976  tposf12  6166  enssdom  6656  mapen  6740  ssenen  6745  phplem4  6749  phplem4on  6761  fidceq  6763  en2eqpr  6801  fiintim  6817  f1finf1o  6835  preimaf1ofi  6839  isotilem  6893  inresflem  6945  casefun  6970  endjusym  6981  dju1p1e2  7053  frec2uzled  10202  iseqf1olemnab  10261  iseqf1olemab  10262  iseqf1olemnanb  10263  hashen  10530  hashfacen  10579  negfi  10999  fisumss  11161  phimullem  11901  ctinfom  11941  hmeoopn  12480  hmeocld  12481  hmeontr  12482  hmeoimaf1o  12483