Theorem f1of 5572

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 5571	. 2 |- ( F : A -1-1-onto-> B -> F : A -1-1-> B )
2		f1f 5531	. 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 5314   -1-1->wf1 5315   -1-1-onto->wf1o 5317

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 5323  df-f1o 5325

This theorem is referenced by:  f1ofn  5573  f1oabexg  5584  f1ompt  5786  f1oresrab  5800  fsn  5807  fsnunf  5839  f1ocnvfv1  5901  f1ocnvfv2  5902  f1ocnvdm  5905  fcof1o  5913  isocnv  5935  isores2  5937  isotr  5940  isopolem  5946  isosolem  5948  f1oiso2  5951  f1ofveu  5989  smoiso  6448  mapsn  6837  f1oen2g  6906  en1  6951  enm  6979  mapen  7007  fidceq  7031  dif1en  7041  fin0  7047  fin0or  7048  ac6sfi  7060  en2eqpr  7069  fiintim  7093  isotilem  7173  supisoex  7176  supisoti  7177  ordiso2  7202  caseinl  7258  caseinr  7259  omp1eomlem  7261  ctm  7276  enomnilem  7305  enmkvlem  7328  enwomnilem  7336  pr2cv1  7368  cc3  7454  frecuzrdgg  10638  fnn0nninf  10660  fxnn0nninf  10661  0tonninf  10662  1tonninf  10663  iseqf1olemkle  10719  iseqf1olemklt  10720  iseqf1olemqcl  10721  iseqf1olemnab  10723  iseqf1olemmo  10727  iseqf1olemqk  10729  iseqf1olemjpcl  10730  iseqf1olemfvp  10732  seq3f1olemqsumkj  10733  seq3f1olemqsumk  10734  seq3f1olemqsum  10735  seq3f1olemstep  10736  seq3f1olemp  10737  seq3f1oleml  10738  seq3f1o  10739  seqf1oglem1  10741  seqf1oglem2  10742  seqf1og  10743  hashfz1  11005  omgadd  11024  hashfacen  11058  leisorel  11059  zfz1isolemiso  11061  seq3coll  11064  cnrecnv  11421  sumeq2  11870  summodclem3  11891  summodclem2a  11892  fsumgcl  11897  fsum3  11898  fsumf1o  11901  fisumss  11903  fsumcl2lem  11909  fsumadd  11917  fsummulc2  11959  prodeq2  12068  prodmodclem3  12086  prodmodclem2a  12087  fprodseq  12094  fprodf1o  12099  fprodssdc  12101  fprodmul  12102  nninfctlemfo  12561  sqpweven  12697  2sqpwodd  12698  phimullem  12747  eulerthlem1  12749  eulerthlemrprm  12751  eulerthlema  12752  eulerthlemh  12753  eulerthlemth  12754  ennnfonelemjn  12973  ennnfonelemp1  12977  ennnfonelemhdmp1  12980  ennnfonelemss  12981  ennnfonelemkh  12983  ennnfonelemhf1o  12984  ennnfonelemex  12985  ennnfonelemnn0  12993  ennnfonelemim  12995  ctinfomlemom  12998  ctiunctlemudc  13008  ctiunctlemfo  13010  ssnnctlemct  13017  idmhm  13502  mhmf1o  13503  idghm  13796  ghmf1o  13812  gsumfzreidx  13874  psrnegcl  14647  psrlinv  14648  ssidcn  14884  txhmeo  14993  dvid  15369  dvidre  15371  dvexp  15385  dfrelog  15534  relogcl  15536  uspgriedgedg  15977  012of  16357  2o01f  16358  iswomninnlem  16417