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

Theorem f1of 5253
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 5252 . 2  |-  ( F : A -1-1-onto-> B  ->  F : A -1-1-> B )
2 f1f 5216 . 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 5011   -1-1->wf1 5012   -1-1-onto->wf1o 5014
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104
This theorem depends on definitions:  df-bi 115  df-f1 5020  df-f1o 5022
This theorem is referenced by:  f1ofn  5254  f1oabexg  5265  f1ompt  5450  f1oresrab  5463  fsn  5469  fsnunf  5497  f1ocnvfv1  5556  f1ocnvfv2  5557  f1ocnvdm  5560  fcof1o  5568  isocnv  5590  isores2  5592  isotr  5595  isopolem  5601  isosolem  5603  f1oiso2  5606  f1ofveu  5640  smoiso  6067  mapsn  6447  f1oen2g  6472  en1  6516  enm  6536  mapen  6562  fidceq  6585  dif1en  6595  fin0  6601  fin0or  6602  ac6sfi  6614  en2eqpr  6623  fiintim  6639  isotilem  6701  supisoex  6704  supisoti  6705  ordiso2  6728  djuin  6756  enomnilem  6794  frecuzrdgg  9823  fnn0nninf  9843  fxnn0nninf  9844  0tonninf  9845  1tonninf  9846  iseqf1olemkle  9913  iseqf1olemklt  9914  iseqf1olemqcl  9915  iseqf1olemnab  9917  iseqf1olemmo  9921  iseqf1olemqk  9923  iseqf1olemjpcl  9924  iseqf1olemfvp  9926  seq3f1olemqsumkj  9927  seq3f1olemqsumk  9928  seq3f1olemqsum  9929  seq3f1olemstep  9930  seq3f1olemp  9931  seq3f1oleml  9932  seq3f1o  9933  hashfz1  10191  omgadd  10210  hashfacen  10241  leisorel  10242  zfz1isolemiso  10244  iseqcoll  10247  cnrecnv  10344  sumeq2  10748  isummolem3  10770  isummolem2a  10771  fsumgcl  10777  fisum  10778  fsumf1o  10782  fisumss  10784  fsumcl2lem  10792  fsumadd  10800  fsummulc2  10842  sqpweven  11431  2sqpwodd  11432  phimullem  11479
  Copyright terms: Public domain W3C validator