Theorem f1of 5642

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 5641	. 2 |- ( F : A -1-1-onto-> B -> F : A -1-1-> B )
2		f1f 5601	. 2 |- ( F : A -1-1-> B -> F : A --> B )
3	1, 2	syl 14	1 |- ( F : A -1-1-onto-> B -> F : A --> B )

This proof depends on syntax axioms:   -> wi 4   -->wf 5376   -1-1->wf1 5377   -1-1-onto->wf1o 5379

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117  df-f1 5385  df-f1o 5387

This theorem is used by:  f1ofn  5643  f1oabexg  5654  f1ompt  5862  f1oresrab  5876  fsn  5883  fsnunf  5918  f1ocnvfv1  5986  f1ocnvfv2  5987  f1ocnvdm  5990  fcof1o  5998  isocnv  6020  isores2  6022  isotr  6025  isopolem  6031  isosolem  6033  f1oiso2  6036  f1ofveu  6076  suppsnopdc  6494  smoiso  6577  mapsnd  6974  mapsn  6976  f1oen2g  7045  en1  7090  enm  7122  mapen  7150  fidceq  7175  dif1en  7187  fin0  7193  fin0or  7194  ac6sfi  7206  en2eqpr  7218  fiintim  7242  isotilem  7352  supisoex  7355  supisoti  7356  ordiso2  7381  caseinl  7437  caseinr  7438  omp1eomlem  7440  ctm  7455  enomnilem  7484  enmkvlem  7507  enwomnilem  7515  pr2cv1  7547  cc3  7640  frecuzrdgg  10874  fnn0nninf  10896  fxnn0nninf  10897  0tonninf  10898  1tonninf  10899  iseqf1olemkle  10955  iseqf1olemklt  10956  iseqf1olemqcl  10957  iseqf1olemnab  10959  iseqf1olemmo  10963  iseqf1olemqk  10965  iseqf1olemjpcl  10966  iseqf1olemfvp  10968  seq3f1olemqsumkj  10969  seq3f1olemqsumk  10970  seq3f1olemqsum  10971  seq3f1olemstep  10972  seq3f1olemp  10973  seq3f1oleml  10974  seq3f1o  10975  seqf1oglem1  10977  seqf1oglem2  10978  seqf1og  10979  hashfz1  11244  omgadd  11264  hashfacen  11306  hashf1lem1  11307  leisorel  11311  zfz1isolemiso  11313  seq3coll  11316  cnrecnv  11698  sumeq2  12150  summodclem3  12172  summodclem2a  12173  fsumgcl  12178  fsum3  12179  fsumf1o  12182  fisumss  12184  fsumcl2lem  12190  fsumadd  12198  fsummulc2  12240  prodeq2  12349  prodmodclem3  12367  prodmodclem2a  12368  fprodseq  12375  fprodf1o  12380  fprodssdc  12382  fprodmul  12383  nninfctlemfo  12842  sqpweven  12980  2sqpwodd  12981  phimullem  13032  eulerthlem1  13034  eulerthlemrprm  13036  eulerthlema  13037  eulerthlemh  13038  eulerthlemth  13039  ballotfilemsima  13317  ennnfonelemjn  13351  ennnfonelemp1  13355  ennnfonelemhdmp1  13358  ennnfonelemss  13359  ennnfonelemkh  13361  ennnfonelemhf1o  13362  ennnfonelemex  13363  ennnfonelemnn0  13371  ennnfonelemim  13373  ctinfomlemom  13376  ctiunctlemudc  13386  ctiunctlemfo  13388  ssnnctlemct  13395  idmhm  13835  mhmf1o  13836  idghm  14121  ghmf1o  14137  gzsumreidx  14231  gzsumshift  14239  gsumvalfi  14242  gsump1  14247  gsumf1ofi  14250  gsummhmfi  14264  gsumressfi  14267  gsumcom2fi  14275  psrass1filem  15177  psrnegcl  15193  psrlinv  15194  ssidcn  15436  txhmeo  15545  dvid  15921  dvidre  15923  dvexp  15937  dfrelog  16089  relogcl  16091  uspgriedgedg  16625  012of  17228  2o01f  17229  iswomninnlem  17306