Theorem f1of1 5582

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

Syntax hints:   → wi 4  –1-1→wf1 5323  –onto→wfo 5324  –1-1-onto→wf1o 5325

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 5333

This theorem is referenced by:  f1of  5583  f1sng  5627  f1oresrab  5812  f1ocnvfvrneq  5923  isores3  5956  isoini2  5960  f1oiso  5967  f1opw2  6229  tposf12  6435  enssdom  6935  mapen  7032  ssenen  7037  phplem4  7041  phplem4on  7054  fidceq  7056  en2eqpr  7099  fiintim  7123  f1finf1o  7146  preimaf1ofi  7150  isotilem  7205  inresflem  7259  casefun  7284  endjusym  7295  pr2cv1  7400  dju1p1e2  7408  frec2uzled  10692  iseqf1olemnab  10764  iseqf1olemab  10765  iseqf1olemnanb  10766  seqf1oglem1  10782  hashen  11047  hashfacen  11101  negfi  11806  fisumss  11971  fprodssdc  12169  phimullem  12815  eulerthlemh  12821  ctinfom  13067  ssnnctlemct  13085  f1ocpbllem  13411  f1ovscpbl  13413  xpsff1o2  13452  eqgen  13832  conjsubgen  13883  hmeoopn  15054  hmeocld  15055  hmeontr  15056  hmeoimaf1o  15057  usgrf1  16045  uspgr2wlkeq  16235  trlres  16260  iswomninnlem  16705