Theorem f1of 5614

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 5613	. 2 |- ( F : A -1-1-onto-> B -> F : A -1-1-> B )
2		f1f 5573	. 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 5348   -1-1->wf1 5349   -1-1-onto->wf1o 5351

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 5357  df-f1o 5359

This theorem is referenced by:  f1ofn  5615  f1oabexg  5626  f1ompt  5828  f1oresrab  5842  fsn  5849  fsnunf  5884  f1ocnvfv1  5950  f1ocnvfv2  5951  f1ocnvdm  5954  fcof1o  5962  isocnv  5984  isores2  5986  isotr  5989  isopolem  5995  isosolem  5997  f1oiso2  6000  f1ofveu  6038  suppsnopdc  6450  smoiso  6533  mapsnd  6923  mapsn  6925  f1oen2g  6994  en1  7039  enm  7071  mapen  7099  fidceq  7124  dif1en  7136  fin0  7142  fin0or  7143  ac6sfi  7155  en2eqpr  7167  fiintim  7191  isotilem  7297  supisoex  7300  supisoti  7301  ordiso2  7326  caseinl  7382  caseinr  7383  omp1eomlem  7385  ctm  7400  enomnilem  7429  enmkvlem  7452  enwomnilem  7460  pr2cv1  7492  cc3  7582  frecuzrdgg  10778  fnn0nninf  10800  fxnn0nninf  10801  0tonninf  10802  1tonninf  10803  iseqf1olemkle  10859  iseqf1olemklt  10860  iseqf1olemqcl  10861  iseqf1olemnab  10863  iseqf1olemmo  10867  iseqf1olemqk  10869  iseqf1olemjpcl  10870  iseqf1olemfvp  10872  seq3f1olemqsumkj  10873  seq3f1olemqsumk  10874  seq3f1olemqsum  10875  seq3f1olemstep  10876  seq3f1olemp  10877  seq3f1oleml  10878  seq3f1o  10879  seqf1oglem1  10881  seqf1oglem2  10882  seqf1og  10883  hashfz1  11146  omgadd  11166  hashfacen  11208  leisorel  11209  zfz1isolemiso  11211  seq3coll  11214  cnrecnv  11595  sumeq2  12044  summodclem3  12066  summodclem2a  12067  fsumgcl  12072  fsum3  12073  fsumf1o  12076  fisumss  12078  fsumcl2lem  12084  fsumadd  12092  fsummulc2  12134  prodeq2  12243  prodmodclem3  12261  prodmodclem2a  12262  fprodseq  12269  fprodf1o  12274  fprodssdc  12276  fprodmul  12277  nninfctlemfo  12736  sqpweven  12872  2sqpwodd  12873  phimullem  12922  eulerthlem1  12924  eulerthlemrprm  12926  eulerthlema  12927  eulerthlemh  12928  eulerthlemth  12929  ennnfonelemjn  13153  ennnfonelemp1  13157  ennnfonelemhdmp1  13160  ennnfonelemss  13161  ennnfonelemkh  13163  ennnfonelemhf1o  13164  ennnfonelemex  13165  ennnfonelemnn0  13173  ennnfonelemim  13175  ctinfomlemom  13178  ctiunctlemudc  13188  ctiunctlemfo  13190  ssnnctlemct  13197  idmhm  13682  mhmf1o  13683  idghm  13976  ghmf1o  13992  gsumfzreidx  14054  psrnegcl  14838  psrlinv  14839  ssidcn  15075  txhmeo  15184  dvid  15560  dvidre  15562  dvexp  15576  dfrelog  15725  relogcl  15727  uspgriedgedg  16174  012of  16767  2o01f  16768  iswomninnlem  16834  gfsumval  16862  gsumgfsumlem  16865  gfsump1  16868