Theorem f1of 5442

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 5441	. 2 |- ( F : A -1-1-onto-> B -> F : A -1-1-> B )
2		f1f 5403	. 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 5194   -1-1->wf1 5195   -1-1-onto->wf1o 5197

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116  df-f1 5203  df-f1o 5205

This theorem is referenced by:  f1ofn  5443  f1oabexg  5454  f1ompt  5647  f1oresrab  5661  fsn  5668  fsnunf  5696  f1ocnvfv1  5756  f1ocnvfv2  5757  f1ocnvdm  5760  fcof1o  5768  isocnv  5790  isores2  5792  isotr  5795  isopolem  5801  isosolem  5803  f1oiso2  5806  f1ofveu  5841  smoiso  6281  mapsn  6668  f1oen2g  6733  en1  6777  enm  6798  mapen  6824  fidceq  6847  dif1en  6857  fin0  6863  fin0or  6864  ac6sfi  6876  en2eqpr  6885  fiintim  6906  isotilem  6983  supisoex  6986  supisoti  6987  ordiso2  7012  caseinl  7068  caseinr  7069  omp1eomlem  7071  ctm  7086  enomnilem  7114  enmkvlem  7137  enwomnilem  7145  cc3  7230  frecuzrdgg  10372  fnn0nninf  10393  fxnn0nninf  10394  0tonninf  10395  1tonninf  10396  iseqf1olemkle  10440  iseqf1olemklt  10441  iseqf1olemqcl  10442  iseqf1olemnab  10444  iseqf1olemmo  10448  iseqf1olemqk  10450  iseqf1olemjpcl  10451  iseqf1olemfvp  10453  seq3f1olemqsumkj  10454  seq3f1olemqsumk  10455  seq3f1olemqsum  10456  seq3f1olemstep  10457  seq3f1olemp  10458  seq3f1oleml  10459  seq3f1o  10460  hashfz1  10717  omgadd  10737  hashfacen  10771  leisorel  10772  zfz1isolemiso  10774  seq3coll  10777  cnrecnv  10874  sumeq2  11322  summodclem3  11343  summodclem2a  11344  fsumgcl  11349  fsum3  11350  fsumf1o  11353  fisumss  11355  fsumcl2lem  11361  fsumadd  11369  fsummulc2  11411  prodeq2  11520  prodmodclem3  11538  prodmodclem2a  11539  fprodseq  11546  fprodf1o  11551  fprodssdc  11553  fprodmul  11554  sqpweven  12129  2sqpwodd  12130  phimullem  12179  eulerthlem1  12181  eulerthlemrprm  12183  eulerthlema  12184  eulerthlemh  12185  eulerthlemth  12186  ennnfonelemjn  12357  ennnfonelemp1  12361  ennnfonelemhdmp1  12364  ennnfonelemss  12365  ennnfonelemkh  12367  ennnfonelemhf1o  12368  ennnfonelemex  12369  ennnfonelemnn0  12377  ennnfonelemim  12379  ctinfomlemom  12382  ctiunctlemudc  12392  ctiunctlemfo  12394  ssnnctlemct  12401  idmhm  12692  mhmf1o  12693  ssidcn  13004  txhmeo  13113  dvid  13456  dvexp  13469  dfrelog  13575  relogcl  13577  012of  14028  2o01f  14029  iswomninnlem  14081