Theorem f1of 5571

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 5570	. 2 |- ( F : A -1-1-onto-> B -> F : A -1-1-> B )
2		f1f 5530	. 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 5313   -1-1->wf1 5314   -1-1-onto->wf1o 5316

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 5322  df-f1o 5324

This theorem is referenced by:  f1ofn  5572  f1oabexg  5583  f1ompt  5785  f1oresrab  5799  fsn  5806  fsnunf  5838  f1ocnvfv1  5900  f1ocnvfv2  5901  f1ocnvdm  5904  fcof1o  5912  isocnv  5934  isores2  5936  isotr  5939  isopolem  5945  isosolem  5947  f1oiso2  5950  f1ofveu  5988  smoiso  6446  mapsn  6835  f1oen2g  6904  en1  6949  enm  6975  mapen  7003  fidceq  7027  dif1en  7037  fin0  7043  fin0or  7044  ac6sfi  7056  en2eqpr  7065  fiintim  7089  isotilem  7169  supisoex  7172  supisoti  7173  ordiso2  7198  caseinl  7254  caseinr  7255  omp1eomlem  7257  ctm  7272  enomnilem  7301  enmkvlem  7324  enwomnilem  7332  pr2cv1  7364  cc3  7450  frecuzrdgg  10633  fnn0nninf  10655  fxnn0nninf  10656  0tonninf  10657  1tonninf  10658  iseqf1olemkle  10714  iseqf1olemklt  10715  iseqf1olemqcl  10716  iseqf1olemnab  10718  iseqf1olemmo  10722  iseqf1olemqk  10724  iseqf1olemjpcl  10725  iseqf1olemfvp  10727  seq3f1olemqsumkj  10728  seq3f1olemqsumk  10729  seq3f1olemqsum  10730  seq3f1olemstep  10731  seq3f1olemp  10732  seq3f1oleml  10733  seq3f1o  10734  seqf1oglem1  10736  seqf1oglem2  10737  seqf1og  10738  hashfz1  11000  omgadd  11019  hashfacen  11053  leisorel  11054  zfz1isolemiso  11056  seq3coll  11059  cnrecnv  11416  sumeq2  11865  summodclem3  11886  summodclem2a  11887  fsumgcl  11892  fsum3  11893  fsumf1o  11896  fisumss  11898  fsumcl2lem  11904  fsumadd  11912  fsummulc2  11954  prodeq2  12063  prodmodclem3  12081  prodmodclem2a  12082  fprodseq  12089  fprodf1o  12094  fprodssdc  12096  fprodmul  12097  nninfctlemfo  12556  sqpweven  12692  2sqpwodd  12693  phimullem  12742  eulerthlem1  12744  eulerthlemrprm  12746  eulerthlema  12747  eulerthlemh  12748  eulerthlemth  12749  ennnfonelemjn  12968  ennnfonelemp1  12972  ennnfonelemhdmp1  12975  ennnfonelemss  12976  ennnfonelemkh  12978  ennnfonelemhf1o  12979  ennnfonelemex  12980  ennnfonelemnn0  12988  ennnfonelemim  12990  ctinfomlemom  12993  ctiunctlemudc  13003  ctiunctlemfo  13005  ssnnctlemct  13012  idmhm  13497  mhmf1o  13498  idghm  13791  ghmf1o  13807  gsumfzreidx  13869  psrnegcl  14641  psrlinv  14642  ssidcn  14878  txhmeo  14987  dvid  15363  dvidre  15365  dvexp  15379  dfrelog  15528  relogcl  15530  uspgriedgedg  15971  012of  16316  2o01f  16317  iswomninnlem  16376