Theorem f1of1 5374

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

Syntax hints:   → wi 4  –1-1→wf1 5128  –onto→wfo 5129  –1-1-onto→wf1o 5130

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 5138

This theorem is referenced by:  f1of  5375  f1sng  5417  f1oresrab  5593  f1ocnvfvrneq  5691  isores3  5724  isoini2  5728  f1oiso  5735  f1opw2  5984  tposf12  6174  enssdom  6664  mapen  6748  ssenen  6753  phplem4  6757  phplem4on  6769  fidceq  6771  en2eqpr  6809  fiintim  6825  f1finf1o  6843  preimaf1ofi  6847  isotilem  6901  inresflem  6953  casefun  6978  endjusym  6989  dju1p1e2  7070  frec2uzled  10233  iseqf1olemnab  10292  iseqf1olemab  10293  iseqf1olemnanb  10294  hashen  10562  hashfacen  10611  negfi  11031  fisumss  11193  phimullem  11937  ctinfom  11977  hmeoopn  12519  hmeocld  12520  hmeontr  12521  hmeoimaf1o  12522  iswomninnlem  13417