Theorem f1of1 5515

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

Syntax hints:   → wi 4  –1-1→wf1 5265  –onto→wfo 5266  –1-1-onto→wf1o 5267

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 5275

This theorem is referenced by:  f1of  5516  f1sng  5558  f1oresrab  5739  f1ocnvfvrneq  5841  isores3  5874  isoini2  5878  f1oiso  5885  f1opw2  6142  tposf12  6345  enssdom  6839  mapen  6925  ssenen  6930  phplem4  6934  phplem4on  6946  fidceq  6948  en2eqpr  6986  fiintim  7010  f1finf1o  7031  preimaf1ofi  7035  isotilem  7090  inresflem  7144  casefun  7169  endjusym  7180  dju1p1e2  7287  frec2uzled  10555  iseqf1olemnab  10627  iseqf1olemab  10628  iseqf1olemnanb  10629  seqf1oglem1  10645  hashen  10910  hashfacen  10962  negfi  11458  fisumss  11622  fprodssdc  11820  phimullem  12466  eulerthlemh  12472  ctinfom  12718  ssnnctlemct  12736  f1ocpbllem  13060  f1ovscpbl  13062  xpsff1o2  13101  eqgen  13481  conjsubgen  13532  hmeoopn  14701  hmeocld  14702  hmeontr  14703  hmeoimaf1o  14704  iswomninnlem  15852