Theorem f1of1 5410

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 5174	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))
2	1	simplbi 272	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴–1-1→𝐵)

Syntax hints:   → wi 4  –1-1→wf1 5164  –onto→wfo 5165  –1-1-onto→wf1o 5166

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 5174

This theorem is referenced by:  f1of  5411  f1sng  5453  f1oresrab  5629  f1ocnvfvrneq  5727  isores3  5760  isoini2  5764  f1oiso  5771  f1opw2  6020  tposf12  6210  enssdom  6700  mapen  6784  ssenen  6789  phplem4  6793  phplem4on  6805  fidceq  6807  en2eqpr  6845  fiintim  6866  f1finf1o  6884  preimaf1ofi  6888  isotilem  6942  inresflem  6994  casefun  7019  endjusym  7030  dju1p1e2  7115  frec2uzled  10310  iseqf1olemnab  10369  iseqf1olemab  10370  iseqf1olemnanb  10371  hashen  10640  hashfacen  10689  negfi  11109  fisumss  11271  fprodssdc  11469  phimullem  12077  eulerthlemh  12083  ctinfom  12129  hmeoopn  12671  hmeocld  12672  hmeontr  12673  hmeoimaf1o  12674  iswomninnlem  13582