Theorem f1of1 3694

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 3203	. 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 3185  -onto->wfo 3186  -1-1-onto->wf1o 3187

This theorem is referenced by:  f1of 3695  isowe 3909  f1oiso 3910  enssdom 4389  mapenlem2 4496  ssenen 4510  phplem4 4517  php3 4521  php3OLD 4522  ssfi 4547  ssfiOLD 4548  unifiOLD 4570  fiint 4572  fiintOLD 4573  unbenlem 7505  infxpidmlem7 7559  eff1i 8739  adjbd1o 10013  ghomf1olem 10391  f2imacnv 10464  homcard 10525

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 3203

Copyright terms: Public domain