Theorem f1of 5360

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 5359	. 2 |- ( F : A -1-1-onto-> B -> F : A -1-1-> B )
2		f1f 5323	. 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 5114   -1-1->wf1 5115   -1-1-onto->wf1o 5117

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

This theorem depends on definitions:  df-bi 116  df-f1 5123  df-f1o 5125

This theorem is referenced by:  f1ofn  5361  f1oabexg  5372  f1ompt  5564  f1oresrab  5578  fsn  5585  fsnunf  5613  f1ocnvfv1  5671  f1ocnvfv2  5672  f1ocnvdm  5675  fcof1o  5683  isocnv  5705  isores2  5707  isotr  5710  isopolem  5716  isosolem  5718  f1oiso2  5721  f1ofveu  5755  smoiso  6192  mapsn  6577  f1oen2g  6642  en1  6686  enm  6707  mapen  6733  fidceq  6756  dif1en  6766  fin0  6772  fin0or  6773  ac6sfi  6785  en2eqpr  6794  fiintim  6810  isotilem  6886  supisoex  6889  supisoti  6890  ordiso2  6913  caseinl  6969  caseinr  6970  omp1eomlem  6972  ctm  6987  enomnilem  7003  frecuzrdgg  10182  fnn0nninf  10203  fxnn0nninf  10204  0tonninf  10205  1tonninf  10206  iseqf1olemkle  10250  iseqf1olemklt  10251  iseqf1olemqcl  10252  iseqf1olemnab  10254  iseqf1olemmo  10258  iseqf1olemqk  10260  iseqf1olemjpcl  10261  iseqf1olemfvp  10263  seq3f1olemqsumkj  10264  seq3f1olemqsumk  10265  seq3f1olemqsum  10266  seq3f1olemstep  10267  seq3f1olemp  10268  seq3f1oleml  10269  seq3f1o  10270  hashfz1  10522  omgadd  10541  hashfacen  10572  leisorel  10573  zfz1isolemiso  10575  seq3coll  10578  cnrecnv  10675  sumeq2  11121  summodclem3  11142  summodclem2a  11143  fsumgcl  11148  fsum3  11149  fsumf1o  11152  fisumss  11154  fsumcl2lem  11160  fsumadd  11168  fsummulc2  11210  prodeq2  11319  sqpweven  11842  2sqpwodd  11843  phimullem  11890  ennnfonelemjn  11904  ennnfonelemp1  11908  ennnfonelemhdmp1  11911  ennnfonelemss  11912  ennnfonelemkh  11914  ennnfonelemhf1o  11915  ennnfonelemex  11916  ennnfonelemnn0  11924  ennnfonelemim  11926  ctinfomlemom  11929  ctiunctlemudc  11939  ctiunctlemfo  11941  ssidcn  12368  txhmeo  12477  dvid  12820  dvexp  12833  isomninnlem  13214