Theorem f1of 2800

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

Assertion

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

Proof of Theorem f1of

Step	Hyp	Ref	Expression
1		f1of1 2799	. 2 |- (F:A-1-1-onto->B -> F:A-1-1->B)
2		f1f 2781	. 2 |- (F:A-1-1->B -> F:A-->B)
3	1, 2	syl 12	1 |- (F:A-1-1-onto->B -> F:A-->B)

Syntax hints:   -> wi 2  -->wf 2418  -1-1->wf1 2419  -1-1-onto->wf1o 2421

This theorem is referenced by:  f1ofn 2801  f1imacnv 2814  f1ococnv2 2817  fsn 2895  f1ocnvfv1 2919  f1ocnvfv2 2920  isocnv 2934  isotr 2935  isotrALT 2936  mapsn 3269  en1 3331  mapenlem1 3384  mapenlem2 3385  uzrdgsuc 4659  infxpidmlem9 4941

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-f1 2435  df-f1o 2437

metamath.org