Theorem f1of 3674

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 3673	. 2 |- (F:A-1-1-onto->B -> F:A-1-1->B)
2		f1f 3650	. 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 3168  -1-1->wf1 3169  -1-1-onto->wf1o 3171

This theorem is referenced by:  f1ofn 3675  f1oabexg 3685  f1imacnv 3690  f1ococnv2 3693  fsn 3819  fopabsn 3825  f1ocnvfv1 3863  f1ocnvfv2 3864  f1ofveu 3867  f1ocnvfv3 3868  f1ocnvdm 3869  isocnv 3881  isotr 3882  isotrALT 3883  mapsn 4329  f1oen2g 4375  en1 4407  mapenlem1 4469  mapenlem2 4470  unifi 4532  uzrdgsuc 6241  uzrdgfnuz 6243  acdc2lem2 7431  acdc5lem2 7434  unbenlem 7447  infxpidmlem9 7503  grpsn 8061  ablsn 8062  shftefif1olem 8661  shftefif1olemOLD 8662  effoi 8666  effoiOLD 8667  logclt 8680  relogclt 8681  dmadjrnt 9738  unopnormt 9757  unopadjt 9759  unoplint 9760  counopt 9761  idcnop 9821  idhmop 9822  unopbdt 9855  bracnlnt 9955  cnvbravalt 9956  leopnmidt 9982  nmopleidt 9983  hmopidmcht 9992  hmopidmpjt 9993  ghomsn 10293  elsymgrn 10306  symggrpiOLD 10311  symgidiOLD 10312  symggrpi 10313  symgidi 10314  cayleylem2 10317  homeofval 10403  hmeogrp 10425  1alg 10498

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 3185  df-f1o 3187

Copyright terms: Public domain