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  6578  mapsnd  6976  mapsn  6978  f1oen2g  7047  en1  7092  enm  7124  mapen  7152  fidceq  7177  dif1en  7189  fin0  7195  fin0or  7196  ac6sfi  7208  en2eqpr  7220  fiintim  7244  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  10873  fnn0nninf  10895  fxnn0nninf  10896  0tonninf  10897  1tonninf  10898  iseqf1olemkle  10954  iseqf1olemklt  10955  iseqf1olemqcl  10956  iseqf1olemnab  10958  iseqf1olemmo  10962  iseqf1olemqk  10964  iseqf1olemjpcl  10965  iseqf1olemfvp  10967  seq3f1olemqsumkj  10968  seq3f1olemqsumk  10969  seq3f1olemqsum  10970  seq3f1olemstep  10971  seq3f1olemp  10972  seq3f1oleml  10973  seq3f1o  10974  seqf1oglem1  10976  seqf1oglem2  10977  seqf1og  10978  hashfz1  11243  omgadd  11263  hashfacen  11305  hashf1lem1  11306  leisorel  11310  zfz1isolemiso  11312  seq3coll  11315  cnrecnv  11697  sumeq2  12149  summodclem3  12171  summodclem2a  12172  fsumgcl  12177  fsum3  12178  fsumf1o  12181  fisumss  12183  fsumcl2lem  12189  fsumadd  12197  fsummulc2  12239  prodeq2  12348  prodmodclem3  12366  prodmodclem2a  12367  fprodseq  12374  fprodf1o  12379  fprodssdc  12381  fprodmul  12382  nninfctlemfo  12841  sqpweven  12979  2sqpwodd  12980  phimullem  13031  eulerthlem1  13033  eulerthlemrprm  13035  eulerthlema  13036  eulerthlemh  13037  eulerthlemth  13038  ballotfilemsima  13316  ennnfonelemjn  13350  ennnfonelemp1  13354  ennnfonelemhdmp1  13357  ennnfonelemss  13358  ennnfonelemkh  13360  ennnfonelemhf1o  13361  ennnfonelemex  13362  ennnfonelemnn0  13370  ennnfonelemim  13372  ctinfomlemom  13375  ctiunctlemudc  13385  ctiunctlemfo  13387  ssnnctlemct  13394  idmhm  13834  mhmf1o  13835  idghm  14120  ghmf1o  14136  gzsumreidx  14230  gzsumshift  14238  gsumvalfi  14241  gsump1  14246  gsumf1ofi  14249  gsummhmfi  14263  gsumressfi  14266  gsumcom2fi  14274  psrass1filem  15186  psrnegcl  15202  psrlinv  15203  ssidcn  15453  txhmeo  15562  dvid  15938  dvidre  15940  dvexp  15954  dfrelog  16106  relogcl  16108  uspgriedgedg  16642  012of  17245  2o01f  17246  iswomninnlem  17323