Theorem f1of 5574

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 5573	. 2 |- ( F : A -1-1-onto-> B -> F : A -1-1-> B )
2		f1f 5533	. 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  5575  f1oabexg  5586  f1ompt  5788  f1oresrab  5802  fsn  5809  fsnunf  5843  f1ocnvfv1  5907  f1ocnvfv2  5908  f1ocnvdm  5911  fcof1o  5919  isocnv  5941  isores2  5943  isotr  5946  isopolem  5952  isosolem  5954  f1oiso2  5957  f1ofveu  5995  smoiso  6454  mapsn  6845  f1oen2g  6914  en1  6959  enm  6987  mapen  7015  fidceq  7039  dif1en  7049  fin0  7055  fin0or  7056  ac6sfi  7068  en2eqpr  7080  fiintim  7104  isotilem  7184  supisoex  7187  supisoti  7188  ordiso2  7213  caseinl  7269  caseinr  7270  omp1eomlem  7272  ctm  7287  enomnilem  7316  enmkvlem  7339  enwomnilem  7347  pr2cv1  7379  cc3  7465  frecuzrdgg  10650  fnn0nninf  10672  fxnn0nninf  10673  0tonninf  10674  1tonninf  10675  iseqf1olemkle  10731  iseqf1olemklt  10732  iseqf1olemqcl  10733  iseqf1olemnab  10735  iseqf1olemmo  10739  iseqf1olemqk  10741  iseqf1olemjpcl  10742  iseqf1olemfvp  10744  seq3f1olemqsumkj  10745  seq3f1olemqsumk  10746  seq3f1olemqsum  10747  seq3f1olemstep  10748  seq3f1olemp  10749  seq3f1oleml  10750  seq3f1o  10751  seqf1oglem1  10753  seqf1oglem2  10754  seqf1og  10755  hashfz1  11017  omgadd  11036  hashfacen  11071  leisorel  11072  zfz1isolemiso  11074  seq3coll  11077  cnrecnv  11436  sumeq2  11885  summodclem3  11906  summodclem2a  11907  fsumgcl  11912  fsum3  11913  fsumf1o  11916  fisumss  11918  fsumcl2lem  11924  fsumadd  11932  fsummulc2  11974  prodeq2  12083  prodmodclem3  12101  prodmodclem2a  12102  fprodseq  12109  fprodf1o  12114  fprodssdc  12116  fprodmul  12117  nninfctlemfo  12576  sqpweven  12712  2sqpwodd  12713  phimullem  12762  eulerthlem1  12764  eulerthlemrprm  12766  eulerthlema  12767  eulerthlemh  12768  eulerthlemth  12769  ennnfonelemjn  12988  ennnfonelemp1  12992  ennnfonelemhdmp1  12995  ennnfonelemss  12996  ennnfonelemkh  12998  ennnfonelemhf1o  12999  ennnfonelemex  13000  ennnfonelemnn0  13008  ennnfonelemim  13010  ctinfomlemom  13013  ctiunctlemudc  13023  ctiunctlemfo  13025  ssnnctlemct  13032  idmhm  13517  mhmf1o  13518  idghm  13811  ghmf1o  13827  gsumfzreidx  13889  psrnegcl  14662  psrlinv  14663  ssidcn  14899  txhmeo  15008  dvid  15384  dvidre  15386  dvexp  15400  dfrelog  15549  relogcl  15551  uspgriedgedg  15992  012of  16416  2o01f  16417  iswomninnlem  16477