Theorem f1of1 3688

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 3197	. 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 3179  -onto->wfo 3180  -1-1-onto->wf1o 3181

This theorem is referenced by:  f1of 3689  isowe 3903  f1oiso 3904  enssdom 4383  mapenlem2 4490  ssenen 4504  phplem4 4511  php3 4515  php3OLD 4516  ssfi 4537  ssfiOLD 4538  unifiOLD 4557  fiint 4559  fiintOLD 4560  unbenlem 7504  infxpidmlem7 7558  eff1i 8744  adjbd1o 10018  ghomf1olem 10396  f2imacnv 10475  homcard 10539

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 3197

Copyright terms: Public domain