Theorem f1of1 5460

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

Syntax hints:   → wi 4  –1-1→wf1 5213  –onto→wfo 5214  –1-1-onto→wf1o 5215

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 5223

This theorem is referenced by:  f1of  5461  f1sng  5503  f1oresrab  5681  f1ocnvfvrneq  5782  isores3  5815  isoini2  5819  f1oiso  5826  f1opw2  6076  tposf12  6269  enssdom  6761  mapen  6845  ssenen  6850  phplem4  6854  phplem4on  6866  fidceq  6868  en2eqpr  6906  fiintim  6927  f1finf1o  6945  preimaf1ofi  6949  isotilem  7004  inresflem  7058  casefun  7083  endjusym  7094  dju1p1e2  7195  frec2uzled  10428  iseqf1olemnab  10487  iseqf1olemab  10488  iseqf1olemnanb  10489  hashen  10763  hashfacen  10815  negfi  11235  fisumss  11399  fprodssdc  11597  phimullem  12224  eulerthlemh  12230  ctinfom  12428  ssnnctlemct  12446  f1ocpbllem  12730  f1ovscpbl  12732  xpsff1o2  12769  eqgen  13084  hmeoopn  13747  hmeocld  13748  hmeontr  13749  hmeoimaf1o  13750  iswomninnlem  14733