Theorem f1of1 5618

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

Syntax hints:   → wi 4  –1-1→wf1 5354  –onto→wfo 5355  –1-1-onto→wf1o 5356

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 5364

This theorem is referenced by:  f1of  5619  f1sng  5663  f1oresrab  5847  f1ocnvfvrneq  5961  isores3  5994  isoini2  5998  f1oiso  6005  f1opw2  6269  tposf12  6513  enssdom  7014  mapen  7112  ssenen  7118  phplem4  7122  phplem4on  7135  fidceq  7137  en2eqpr  7180  fiintim  7204  f1finf1o  7230  preimaf1ofi  7234  fsuppcorn  7267  isotilem  7310  inresflem  7364  casefun  7389  endjusym  7400  pr2cv1  7505  dju1p1e2  7513  frec2uzled  10815  iseqf1olemnab  10887  iseqf1olemab  10888  iseqf1olemnanb  10889  seqf1oglem1  10905  hashen  11172  hashfacen  11233  negfi  11938  fisumss  12103  fprodssdc  12301  phimullem  12947  eulerthlemh  12953  ballotfilemscr  13206  ballotfilemro  13210  ballotfilemfrc  13214  ballotfilemrinv0  13220  ctinfom  13263  ssnnctlemct  13281  f1ocpbllem  13574  f1ovscpbl  13576  xpsff1o2  13615  eqgen  13980  conjsubgen  14031  hmeoopn  15302  hmeocld  15303  hmeontr  15304  hmeoimaf1o  15305  usgrf1  16296  uspgr2wlkeq  16486  trlres  16511  iswomninnlem  16960