Theorem f1of1 5633

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

Syntax hints:   → wi 4  –1-1→wf1 5369  –onto→wfo 5370  –1-1-onto→wf1o 5371

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 5379

This theorem is referenced by:  f1of  5634  f1sng  5678  f1oresrab  5864  f1ocnvfvrneq  5978  isores3  6011  isoini2  6015  f1oiso  6022  f1opw2  6286  tposf12  6530  enssdom  7038  mapen  7136  ssenen  7142  phplem4  7146  phplem4on  7159  fidceq  7161  en2eqpr  7204  fiintim  7228  f1finf1o  7254  preimaf1ofi  7258  fsuppcorn  7291  isotilem  7336  inresflem  7390  casefun  7415  endjusym  7426  pr2cv1  7531  dju1p1e2  7539  frec2uzled  10844  iseqf1olemnab  10916  iseqf1olemab  10917  iseqf1olemnanb  10918  seqf1oglem1  10934  hashen  11201  hashfacen  11262  hashf1lem1  11263  negfi  11972  fisumss  12137  fprodssdc  12335  phimullem  12981  eulerthlemh  12987  ballotfilemscr  13240  ballotfilemro  13244  ballotfilemfrc  13248  ballotfilemrinv0  13254  ctinfom  13297  ssnnctlemct  13315  f1ocpbllem  13608  f1ovscpbl  13610  xpsff1o2  13649  eqgen  14007  conjsubgen  14058  hmeoopn  15335  hmeocld  15336  hmeontr  15337  hmeoimaf1o  15338  usgrf1  16330  uspgr2wlkeq  16520  trlres  16545  iswomninnlem  17004