Theorem f1of1 5533

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

Syntax hints:   → wi 4  –1-1→wf1 5277  –onto→wfo 5278  –1-1-onto→wf1o 5279

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 5287

This theorem is referenced by:  f1of  5534  f1sng  5577  f1oresrab  5758  f1ocnvfvrneq  5864  isores3  5897  isoini2  5901  f1oiso  5908  f1opw2  6165  tposf12  6368  enssdom  6866  mapen  6958  ssenen  6963  phplem4  6967  phplem4on  6979  fidceq  6981  en2eqpr  7019  fiintim  7043  f1finf1o  7064  preimaf1ofi  7068  isotilem  7123  inresflem  7177  casefun  7202  endjusym  7213  dju1p1e2  7321  frec2uzled  10596  iseqf1olemnab  10668  iseqf1olemab  10669  iseqf1olemnanb  10670  seqf1oglem1  10686  hashen  10951  hashfacen  11003  negfi  11614  fisumss  11778  fprodssdc  11976  phimullem  12622  eulerthlemh  12628  ctinfom  12874  ssnnctlemct  12892  f1ocpbllem  13217  f1ovscpbl  13219  xpsff1o2  13258  eqgen  13638  conjsubgen  13689  hmeoopn  14858  hmeocld  14859  hmeontr  14860  hmeoimaf1o  14861  iswomninnlem  16129