Theorem f1of 3684

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 3683	. 2 |- (F:A-1-1-onto->B -> F:A-1-1->B)
2		f1f 3660	. 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 3174  -1-1->wf1 3175  -1-1-onto->wf1o 3177

This theorem is referenced by:  f1ofn 3685  f1oabexg 3695  f1imacnv 3700  f1ococnv2 3703  fsn 3829  fopabsn 3835  f1ocnvfv1 3873  f1ocnvfv2 3874  f1ofveu 3877  f1ocnvfv3 3878  f1ocnvdm 3879  isocnv 3891  isotr 3892  isotrALT 3893  mapsn 4338  f1oen2g 4384  en1 4416  mapenlem1 4478  mapenlem2 4479  unifi 4541  uzrdgsuc 6254  uzrdgfnuz 6256  acdc2lem2 7448  acdc5lem2 7451  unbenlem 7464  infxpidmlem9 7520  grpsn 8088  ablsn 8089  shftefif1olem 8696  effoi 8700  logclt 8713  relogclt 8714  dmadjrnt 9778  unopnormt 9798  unopadjt 9800  unoplint 9801  counopt 9802  idcnop 9862  idhmop 9863  unopbdt 9896  bracnlnt 9998  cnvbravalt 9999  leopnmidt 10027  nmopleidt 10028  hmopidmcht 10037  hmopidmpjt 10038  ghomsn 10344  elsymgrn 10357  symggrpi 10362  symgidi 10363  cayleylem2 10366  homeofval 10462  hmeogrp 10484  1alg 10570  idfisf 10670

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 3191  df-f1o 3193

Copyright terms: Public domain