Theorem f1of1 2799

Description: A one-to-one onto mapping is a one-to-one mapping.

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 2437	. 2 |- (F:A-1-1-onto->B <-> (F:A-1-1->B /\ F:A-onto->B))
2	1	pm3.26bd 259	1 |- (F:A-1-1-onto->B -> F:A-1-1->B)

Syntax hints:   -> wi 2  -1-1->wf1 2419  -onto->wfo 2420  -1-1-onto->wf1o 2421

This theorem is referenced by:  f1of 2800  isowe 2941  f1oiso 2942  enssdom 3287  mapenlem2 3385  ssenen 3399  phplem5 3407  php3 3411  ssfi 3430  fiint 3445  infxpidmlem7 4939

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-an 198  df-f1o 2437

metamath.org