Theorem f1of1 5591

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

Syntax hints:   → wi 4  –1-1→wf1 5330  –onto→wfo 5331  –1-1-onto→wf1o 5332

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-f1o 5340

This theorem is referenced by:  f1of  5592  f1sng  5636  f1oresrab  5820  f1ocnvfvrneq  5933  isores3  5966  isoini2  5970  f1oiso  5977  f1opw2  6239  tposf12  6478  enssdom  6978  mapen  7075  ssenen  7080  phplem4  7084  phplem4on  7097  fidceq  7099  en2eqpr  7142  fiintim  7166  f1finf1o  7189  preimaf1ofi  7193  isotilem  7248  inresflem  7302  casefun  7327  endjusym  7338  pr2cv1  7443  dju1p1e2  7451  frec2uzled  10737  iseqf1olemnab  10809  iseqf1olemab  10810  iseqf1olemnanb  10811  seqf1oglem1  10827  hashen  11092  hashfacen  11146  negfi  11851  fisumss  12016  fprodssdc  12214  phimullem  12860  eulerthlemh  12866  ctinfom  13112  ssnnctlemct  13130  f1ocpbllem  13456  f1ovscpbl  13458  xpsff1o2  13497  eqgen  13877  conjsubgen  13928  hmeoopn  15105  hmeocld  15106  hmeontr  15107  hmeoimaf1o  15108  usgrf1  16099  uspgr2wlkeq  16289  trlres  16314  iswomninnlem  16765