Theorem f1of 5432

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 5431	. 2 |- ( F : A -1-1-onto-> B -> F : A -1-1-> B )
2		f1f 5393	. 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 5184   -1-1->wf1 5185   -1-1-onto->wf1o 5187

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 5193  df-f1o 5195

This theorem is referenced by:  f1ofn  5433  f1oabexg  5444  f1ompt  5636  f1oresrab  5650  fsn  5657  fsnunf  5685  f1ocnvfv1  5745  f1ocnvfv2  5746  f1ocnvdm  5749  fcof1o  5757  isocnv  5779  isores2  5781  isotr  5784  isopolem  5790  isosolem  5792  f1oiso2  5795  f1ofveu  5830  smoiso  6270  mapsn  6656  f1oen2g  6721  en1  6765  enm  6786  mapen  6812  fidceq  6835  dif1en  6845  fin0  6851  fin0or  6852  ac6sfi  6864  en2eqpr  6873  fiintim  6894  isotilem  6971  supisoex  6974  supisoti  6975  ordiso2  7000  caseinl  7056  caseinr  7057  omp1eomlem  7059  ctm  7074  enomnilem  7102  enmkvlem  7125  enwomnilem  7133  cc3  7209  frecuzrdgg  10351  fnn0nninf  10372  fxnn0nninf  10373  0tonninf  10374  1tonninf  10375  iseqf1olemkle  10419  iseqf1olemklt  10420  iseqf1olemqcl  10421  iseqf1olemnab  10423  iseqf1olemmo  10427  iseqf1olemqk  10429  iseqf1olemjpcl  10430  iseqf1olemfvp  10432  seq3f1olemqsumkj  10433  seq3f1olemqsumk  10434  seq3f1olemqsum  10435  seq3f1olemstep  10436  seq3f1olemp  10437  seq3f1oleml  10438  seq3f1o  10439  hashfz1  10696  omgadd  10715  hashfacen  10749  leisorel  10750  zfz1isolemiso  10752  seq3coll  10755  cnrecnv  10852  sumeq2  11300  summodclem3  11321  summodclem2a  11322  fsumgcl  11327  fsum3  11328  fsumf1o  11331  fisumss  11333  fsumcl2lem  11339  fsumadd  11347  fsummulc2  11389  prodeq2  11498  prodmodclem3  11516  prodmodclem2a  11517  fprodseq  11524  fprodf1o  11529  fprodssdc  11531  fprodmul  11532  sqpweven  12107  2sqpwodd  12108  phimullem  12157  eulerthlem1  12159  eulerthlemrprm  12161  eulerthlema  12162  eulerthlemh  12163  eulerthlemth  12164  ennnfonelemjn  12335  ennnfonelemp1  12339  ennnfonelemhdmp1  12342  ennnfonelemss  12343  ennnfonelemkh  12345  ennnfonelemhf1o  12346  ennnfonelemex  12347  ennnfonelemnn0  12355  ennnfonelemim  12357  ctinfomlemom  12360  ctiunctlemudc  12370  ctiunctlemfo  12372  ssnnctlemct  12379  ssidcn  12860  txhmeo  12969  dvid  13312  dvexp  13325  dfrelog  13431  relogcl  13433  012of  13885  2o01f  13886  iswomninnlem  13938