ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  f1of Unicode version

Theorem f1of 5373
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
StepHypRef Expression
1 f1of1 5372 . 2  |-  ( F : A -1-1-onto-> B  ->  F : A -1-1-> B )
2 f1f 5334 . 2  |-  ( F : A -1-1-> B  ->  F : A --> B )
31, 2syl 14 1  |-  ( F : A -1-1-onto-> B  ->  F : A
--> B )
Colors of variables: wff set class
Syntax hints:    -> wi 4   -->wf 5125   -1-1->wf1 5126   -1-1-onto->wf1o 5128
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 5134  df-f1o 5136
This theorem is referenced by:  f1ofn  5374  f1oabexg  5385  f1ompt  5577  f1oresrab  5591  fsn  5598  fsnunf  5626  f1ocnvfv1  5684  f1ocnvfv2  5685  f1ocnvdm  5688  fcof1o  5696  isocnv  5718  isores2  5720  isotr  5723  isopolem  5729  isosolem  5731  f1oiso2  5734  f1ofveu  5768  smoiso  6205  mapsn  6590  f1oen2g  6655  en1  6699  enm  6720  mapen  6746  fidceq  6769  dif1en  6779  fin0  6785  fin0or  6786  ac6sfi  6798  en2eqpr  6807  fiintim  6823  isotilem  6899  supisoex  6902  supisoti  6903  ordiso2  6926  caseinl  6982  caseinr  6983  omp1eomlem  6985  ctm  7000  enomnilem  7016  enmkvlem  7041  enwomnilem  7048  cc3  7098  frecuzrdgg  10218  fnn0nninf  10239  fxnn0nninf  10240  0tonninf  10241  1tonninf  10242  iseqf1olemkle  10286  iseqf1olemklt  10287  iseqf1olemqcl  10288  iseqf1olemnab  10290  iseqf1olemmo  10294  iseqf1olemqk  10296  iseqf1olemjpcl  10297  iseqf1olemfvp  10299  seq3f1olemqsumkj  10300  seq3f1olemqsumk  10301  seq3f1olemqsum  10302  seq3f1olemstep  10303  seq3f1olemp  10304  seq3f1oleml  10305  seq3f1o  10306  hashfz1  10559  omgadd  10578  hashfacen  10609  leisorel  10610  zfz1isolemiso  10612  seq3coll  10615  cnrecnv  10712  sumeq2  11158  summodclem3  11179  summodclem2a  11180  fsumgcl  11185  fsum3  11186  fsumf1o  11189  fisumss  11191  fsumcl2lem  11197  fsumadd  11205  fsummulc2  11247  prodeq2  11356  prodmodclem3  11374  prodmodclem2a  11375  sqpweven  11882  2sqpwodd  11883  phimullem  11930  ennnfonelemjn  11944  ennnfonelemp1  11948  ennnfonelemhdmp1  11951  ennnfonelemss  11952  ennnfonelemkh  11954  ennnfonelemhf1o  11955  ennnfonelemex  11956  ennnfonelemnn0  11964  ennnfonelemim  11966  ctinfomlemom  11969  ctiunctlemudc  11979  ctiunctlemfo  11981  ssidcn  12411  txhmeo  12520  dvid  12863  dvexp  12876  dfrelog  12982  relogcl  12984  012of  13356  2o01f  13357  iswomninnlem  13410
  Copyright terms: Public domain W3C validator