Theorem f1of 5323

Description: A one-to-one onto mapping is a mapping. (Contributed by NM, 12-Dec-2003.)

Assertion

Ref	Expression
f1of	|- ( F : A -1-1-onto-> B -> F : A --> B )

Proof of Theorem f1of

Step	Hyp	Ref	Expression
1		f1of1 5322	. 2 |- ( F : A -1-1-onto-> B -> F : A -1-1-> B )
2		f1f 5286	. 2 |- ( F : A -1-1-> B -> F : A --> B )
3	1, 2	syl 14	1 |- ( F : A -1-1-onto-> B -> F : A --> B )

Syntax hints:   -> wi 4   -->wf 5077   -1-1->wf1 5078   -1-1-onto->wf1o 5080

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116  df-f1 5086  df-f1o 5088

This theorem is referenced by:  f1ofn  5324  f1oabexg  5335  f1ompt  5525  f1oresrab  5539  fsn  5546  fsnunf  5574  f1ocnvfv1  5632  f1ocnvfv2  5633  f1ocnvdm  5636  fcof1o  5644  isocnv  5666  isores2  5668  isotr  5671  isopolem  5677  isosolem  5679  f1oiso2  5682  f1ofveu  5716  smoiso  6153  mapsn  6538  f1oen2g  6603  en1  6647  enm  6667  mapen  6693  fidceq  6716  dif1en  6726  fin0  6732  fin0or  6733  ac6sfi  6745  en2eqpr  6754  fiintim  6770  isotilem  6845  supisoex  6848  supisoti  6849  ordiso2  6872  caseinl  6928  caseinr  6929  omp1eomlem  6931  ctm  6946  enomnilem  6960  frecuzrdgg  10082  fnn0nninf  10103  fxnn0nninf  10104  0tonninf  10105  1tonninf  10106  iseqf1olemkle  10150  iseqf1olemklt  10151  iseqf1olemqcl  10152  iseqf1olemnab  10154  iseqf1olemmo  10158  iseqf1olemqk  10160  iseqf1olemjpcl  10161  iseqf1olemfvp  10163  seq3f1olemqsumkj  10164  seq3f1olemqsumk  10165  seq3f1olemqsum  10166  seq3f1olemstep  10167  seq3f1olemp  10168  seq3f1oleml  10169  seq3f1o  10170  hashfz1  10422  omgadd  10441  hashfacen  10472  leisorel  10473  zfz1isolemiso  10475  seq3coll  10478  cnrecnv  10575  sumeq2  11020  summodclem3  11041  summodclem2a  11042  fsumgcl  11047  fsum3  11048  fsumf1o  11051  fisumss  11053  fsumcl2lem  11059  fsumadd  11067  fsummulc2  11109  sqpweven  11698  2sqpwodd  11699  phimullem  11746  ennnfonelemjn  11760  ennnfonelemp1  11764  ennnfonelemhdmp1  11767  ennnfonelemss  11768  ennnfonelemkh  11770  ennnfonelemhf1o  11771  ennnfonelemex  11772  ennnfonelemnn0  11780  ennnfonelemim  11782  ctinfomlemom  11785  ctiunctlemudc  11793  ctiunctlemfo  11795  ssidcn  12221  dvid  12617  isomninnlem  12917