Theorem f1of1 5156

Description: A one-to-one onto mapping is a one-to-one mapping. (Contributed by NM, 12-Dec-2003.)

Assertion

Ref	Expression
f1of1	|- ( F : A -1-1-onto-> B -> F : A -1-1-> B )

Proof of Theorem f1of1

Step	Hyp	Ref	Expression
1		df-f1o 4939	. 2 |- ( F : A -1-1-onto-> B <-> ( F : A -1-1-> B /\ F : A -onto-> B ) )
2	1	simplbi 268	1 |- ( F : A -1-1-onto-> B -> F : A -1-1-> B )

Syntax hints:   -> wi 4   -1-1->wf1 4929   -onto->wfo 4930   -1-1-onto->wf1o 4931

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104

This theorem depends on definitions:  df-bi 115  df-f1o 4939

This theorem is referenced by:  f1of  5157  f1oresrab  5361  f1ocnvfvrneq  5453  isores3  5486  isoini2  5489  f1oiso  5496  f1opw2  5737  tposf12  5918  enssdom  6309  phplem4  6390  phplem4on  6402  fidceq  6404  en2eqpr  6434  isotilem  6478  frec2uzled  9511  sizeen  9808  negfi  10248