Theorem f1of 3689

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 3688	. 2 |- (F:A-1-1-onto->B -> F:A-1-1->B)
2		f1f 3665	. 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 3178  -1-1->wf1 3179  -1-1-onto->wf1o 3181

This theorem is referenced by:  f1ofn 3690  f1oabexg 3700  f1imacnv 3705  f1ococnv2 3708  fsn 3834  fopabsn 3840  f1ocnvfv1 3878  f1ocnvfv2 3879  f1ofveu 3882  f1ocnvfv3 3883  f1ocnvdm 3884  isocnv 3896  isotr 3897  isotrALT 3898  mapsn 4345  f1oen2g 4394  en1 4426  mapenlem1 4489  mapenlem2 4490  unifiOLD 4557  uzrdgsuc 6304  uzrdgfnuz 6306  acdc2lem2 7489  acdc5lem2 7492  unbenlem 7504  infxpidmlem9 7560  grpsn 8124  shftefif1olem 8741  effoi 8745  logclt 8758  relogclt 8759  dmadjrnt 9821  unopnormt 9841  unopadjt 9843  unoplint 9844  counopt 9845  idcnop 9905  idhmop 9906  unopbdt 9940  bracnlnt 10042  cnvbravalt 10043  leopnmidt 10071  nmopleidt 10072  hmopidmcht 10081  hmopidmpjt 10082  ghomsn 10388  elsymgrn 10401  symggrpi 10406  symgidi 10407  cayleylem2 10410  homeofval 10516  hmeogrp 10538  eqindhome 10541  hmeobc 10542  1alg 10654  idfisf 10760

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-f1 3195  df-f1o 3197

Copyright terms: Public domain