Theorem f1of 5426

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 5425	. 2 |- ( F : A -1-1-onto-> B -> F : A -1-1-> B )
2		f1f 5387	. 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 5178   -1-1->wf1 5179   -1-1-onto->wf1o 5181

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 5187  df-f1o 5189

This theorem is referenced by:  f1ofn  5427  f1oabexg  5438  f1ompt  5630  f1oresrab  5644  fsn  5651  fsnunf  5679  f1ocnvfv1  5739  f1ocnvfv2  5740  f1ocnvdm  5743  fcof1o  5751  isocnv  5773  isores2  5775  isotr  5778  isopolem  5784  isosolem  5786  f1oiso2  5789  f1ofveu  5824  smoiso  6261  mapsn  6647  f1oen2g  6712  en1  6756  enm  6777  mapen  6803  fidceq  6826  dif1en  6836  fin0  6842  fin0or  6843  ac6sfi  6855  en2eqpr  6864  fiintim  6885  isotilem  6962  supisoex  6965  supisoti  6966  ordiso2  6991  caseinl  7047  caseinr  7048  omp1eomlem  7050  ctm  7065  enomnilem  7093  enmkvlem  7116  enwomnilem  7124  cc3  7200  frecuzrdgg  10341  fnn0nninf  10362  fxnn0nninf  10363  0tonninf  10364  1tonninf  10365  iseqf1olemkle  10409  iseqf1olemklt  10410  iseqf1olemqcl  10411  iseqf1olemnab  10413  iseqf1olemmo  10417  iseqf1olemqk  10419  iseqf1olemjpcl  10420  iseqf1olemfvp  10422  seq3f1olemqsumkj  10423  seq3f1olemqsumk  10424  seq3f1olemqsum  10425  seq3f1olemstep  10426  seq3f1olemp  10427  seq3f1oleml  10428  seq3f1o  10429  hashfz1  10685  omgadd  10704  hashfacen  10735  leisorel  10736  zfz1isolemiso  10738  seq3coll  10741  cnrecnv  10838  sumeq2  11286  summodclem3  11307  summodclem2a  11308  fsumgcl  11313  fsum3  11314  fsumf1o  11317  fisumss  11319  fsumcl2lem  11325  fsumadd  11333  fsummulc2  11375  prodeq2  11484  prodmodclem3  11502  prodmodclem2a  11503  fprodseq  11510  fprodf1o  11515  fprodssdc  11517  fprodmul  11518  sqpweven  12084  2sqpwodd  12085  phimullem  12134  eulerthlem1  12136  eulerthlemrprm  12138  eulerthlema  12139  eulerthlemh  12140  eulerthlemth  12141  ennnfonelemjn  12272  ennnfonelemp1  12276  ennnfonelemhdmp1  12279  ennnfonelemss  12280  ennnfonelemkh  12282  ennnfonelemhf1o  12283  ennnfonelemex  12284  ennnfonelemnn0  12292  ennnfonelemim  12294  ctinfomlemom  12297  ctiunctlemudc  12307  ctiunctlemfo  12309  ssnnctlemct  12316  ssidcn  12751  txhmeo  12860  dvid  13203  dvexp  13216  dfrelog  13322  relogcl  13324  012of  13709  2o01f  13710  iswomninnlem  13762