Theorem f1of 4635

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 4634	. 2 |- (F:A-1-1-onto->B -> F:A-1-1->B)
2		f1f 4610	. 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 3  -->wf 3994  -1-1->wf1 3995  -1-1-onto->wf1o 3997

This theorem is referenced by:  f1ofn 4636  f1oabexg 4650  f1imacnv 4656  f1ococnv2 4662  fsn 4807  fopabsnOLD 4816  f1ocnvfv1 4854  f1ocnvfv2 4855  f1ofveu 4858  f1ocnvfv3 4859  f1ocnvdm 4860  isocnv 4873  isotr 4874  isotrALT 4875  mapsn 5404  f1oen2g 5453  en1 5485  ac6sfilem3 5508  mapenlem1 5583  mapenlem2 5584  unifi 5648  ordiso 5683  uzrdgsuci 7716  uzrdgfnuzi 7718  acdc2lem2 8758  acdc5lem2 8761  unbenlem 8773  infxpidmlem9 8829  grpsn 9340  shftefif1olem 10095  effoi 10099  logcl 10112  relogcl 10113  elsymgrn 10200  symggrpi 10205  symgidi 10206  homeofval 10234  hmeobc 10239  fbssint 10279  dmadjrn 11458  unopnorm 11478  unopadj 11480  unoplin 11481  counop 11482  idcnop 11542  idhmop 11543  unopbd 11577  bracnln 11680  cnvbraval 11681  leopnmid 11709  nmopleid 11710  hmopidmch 11725  hmopidmpj 11726  ghomsn 13631  cayleylem2 13642  scprefat 14380  dispos 14632  symgfo 14730  hmeogrp 14892  eqindhome 14895  topgrpbs 14974  1alg 15069  idfisf 15189  idsubfun 15206  finsschain 15373  ordisoOLD 15374  fcluscomplem 15620  f1ocan1fv 15717  metf1o 15843  ishomeo2 15896  hmeocn 15897  ismtyval 15947  isismty 15948  ismtyhmeolem 15950  ismtyres 15954  ismrer1 16024  reparpht 16065  rngisocnv 16135  smoiso 16453  pautset 17395  ispaut 17396

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 164  df-an 242  df-f1 4011  df-f1o 4013

Copyright terms: Public domain