Theorem f1of 5592

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 5591	. 2 |- ( F : A -1-1-onto-> B -> F : A -1-1-> B )
2		f1f 5551	. 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 5329   -1-1->wf1 5330   -1-1-onto->wf1o 5332

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

This theorem depends on definitions:  df-bi 117  df-f1 5338  df-f1o 5340

This theorem is referenced by:  f1ofn  5593  f1oabexg  5604  f1ompt  5806  f1oresrab  5820  fsn  5827  fsnunf  5862  f1ocnvfv1  5928  f1ocnvfv2  5929  f1ocnvdm  5932  fcof1o  5940  isocnv  5962  isores2  5964  isotr  5967  isopolem  5973  isosolem  5975  f1oiso2  5978  f1ofveu  6016  suppsnopdc  6428  smoiso  6511  mapsn  6902  f1oen2g  6971  en1  7016  enm  7047  mapen  7075  fidceq  7099  dif1en  7111  fin0  7117  fin0or  7118  ac6sfi  7130  en2eqpr  7142  fiintim  7166  isotilem  7248  supisoex  7251  supisoti  7252  ordiso2  7277  caseinl  7333  caseinr  7334  omp1eomlem  7336  ctm  7351  enomnilem  7380  enmkvlem  7403  enwomnilem  7411  pr2cv1  7443  cc3  7530  frecuzrdgg  10724  fnn0nninf  10746  fxnn0nninf  10747  0tonninf  10748  1tonninf  10749  iseqf1olemkle  10805  iseqf1olemklt  10806  iseqf1olemqcl  10807  iseqf1olemnab  10809  iseqf1olemmo  10813  iseqf1olemqk  10815  iseqf1olemjpcl  10816  iseqf1olemfvp  10818  seq3f1olemqsumkj  10819  seq3f1olemqsumk  10820  seq3f1olemqsum  10821  seq3f1olemstep  10822  seq3f1olemp  10823  seq3f1oleml  10824  seq3f1o  10825  seqf1oglem1  10827  seqf1oglem2  10828  seqf1og  10829  hashfz1  11091  omgadd  11111  hashfacen  11146  leisorel  11147  zfz1isolemiso  11149  seq3coll  11152  cnrecnv  11533  sumeq2  11982  summodclem3  12004  summodclem2a  12005  fsumgcl  12010  fsum3  12011  fsumf1o  12014  fisumss  12016  fsumcl2lem  12022  fsumadd  12030  fsummulc2  12072  prodeq2  12181  prodmodclem3  12199  prodmodclem2a  12200  fprodseq  12207  fprodf1o  12212  fprodssdc  12214  fprodmul  12215  nninfctlemfo  12674  sqpweven  12810  2sqpwodd  12811  phimullem  12860  eulerthlem1  12862  eulerthlemrprm  12864  eulerthlema  12865  eulerthlemh  12866  eulerthlemth  12867  ennnfonelemjn  13086  ennnfonelemp1  13090  ennnfonelemhdmp1  13093  ennnfonelemss  13094  ennnfonelemkh  13096  ennnfonelemhf1o  13097  ennnfonelemex  13098  ennnfonelemnn0  13106  ennnfonelemim  13108  ctinfomlemom  13111  ctiunctlemudc  13121  ctiunctlemfo  13123  ssnnctlemct  13130  idmhm  13615  mhmf1o  13616  idghm  13909  ghmf1o  13925  gsumfzreidx  13987  psrnegcl  14767  psrlinv  14768  ssidcn  15004  txhmeo  15113  dvid  15489  dvidre  15491  dvexp  15505  dfrelog  15654  relogcl  15656  uspgriedgedg  16103  012of  16696  2o01f  16697  iswomninnlem  16765  gfsumval  16792  gsumgfsumlem  16795  gfsump1  16798