Theorem f1of 3765

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 3764	. 2 |- (F:A-1-1-onto->B -> F:A-1-1->B)
2		f1f 3740	. 2 |- (F:A-1-1->B -> F:A-->B)
3	1, 2	syl 10	1 |- (F:A-1-1-onto->B -> F:A-->B)

Syntax hints:   -> wi 3  -->wf 3233  -1-1->wf1 3234  -1-1-onto->wf1o 3236

This theorem is referenced by:  f1ofn 3766  f1oabexg 3776  f1imacnv 3781  f1ococnv2 3784  fsn 3910  fopabsn 3916  f1ocnvfv1 3954  f1ocnvfv2 3955  f1ofveu 3958  f1ocnvfv3 3959  f1ocnvdm 3960  isocnv 3972  isotr 3973  isotrALT 3974  mapsn 4432  f1oen2g 4481  en1 4513  mapenlem1 4578  mapenlem2 4579  unifi 4642  uzrdgsuci 6597  uzrdgfnuzi 6599  acdc2lem2 7614  acdc5lem2 7617  unbenlem 7629  infxpidmlem9 7685  grpsn 8243  shftefif1olem 8860  effoi 8864  logcl 8877  relogcl 8878  dmadjrn 9939  unopnorm 9959  unopadj 9961  unoplin 9962  counop 9963  idcnop 10022  idhmop 10023  unopbd 10057  bracnln 10159  cnvbraval 10160  leopnmid 10188  nmopleid 10189  hmopidmch 10198  hmopidmpj 10199  ghomsn 10509  elsymgrn 10522  symggrpi 10527  symgidi 10528  cayleylem2 10531  homeofval 10652  hmeogrp 10674  eqindhome 10677  hmeobc 10678  1alg 10789  idfisf 10902

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 145  df-an 223  df-f1 3250  df-f1o 3252

Copyright terms: Public domain