Theorem f1of1 3673

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 3187	. 2 |- (F:A-1-1-onto->B <-> (F:A-1-1->B /\ F:A-onto->B))
2	1	pm3.26bi 322	1 |- (F:A-1-1-onto->B -> F:A-1-1->B)

Syntax hints:   -> wi 3  -1-1->wf1 3169  -onto->wfo 3170  -1-1-onto->wf1o 3171

This theorem is referenced by:  f1of 3674  isowe 3888  f1oiso 3889  enssdom 4364  mapenlem2 4470  ssenen 4484  phplem4 4491  php3 4495  ssfi 4515  unifi 4532  fiint 4534  unbenlem 7447  infxpidmlem7 7501  eff1i 8665  adjbd1o 9933  ghomf1olem 10301  f2imacnv 10370  homcard 10426

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

This theorem depends on definitions:  df-bi 147  df-an 225  df-f1o 3187

Copyright terms: Public domain