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

Theorem f1of 5335
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 5334 . 2  |-  ( F : A -1-1-onto-> B  ->  F : A -1-1-> B )
2 f1f 5298 . 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 5089   -1-1->wf1 5090   -1-1-onto->wf1o 5092
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 5098  df-f1o 5100
This theorem is referenced by:  f1ofn  5336  f1oabexg  5347  f1ompt  5539  f1oresrab  5553  fsn  5560  fsnunf  5588  f1ocnvfv1  5646  f1ocnvfv2  5647  f1ocnvdm  5650  fcof1o  5658  isocnv  5680  isores2  5682  isotr  5685  isopolem  5691  isosolem  5693  f1oiso2  5696  f1ofveu  5730  smoiso  6167  mapsn  6552  f1oen2g  6617  en1  6661  enm  6682  mapen  6708  fidceq  6731  dif1en  6741  fin0  6747  fin0or  6748  ac6sfi  6760  en2eqpr  6769  fiintim  6785  isotilem  6861  supisoex  6864  supisoti  6865  ordiso2  6888  caseinl  6944  caseinr  6945  omp1eomlem  6947  ctm  6962  enomnilem  6978  frecuzrdgg  10157  fnn0nninf  10178  fxnn0nninf  10179  0tonninf  10180  1tonninf  10181  iseqf1olemkle  10225  iseqf1olemklt  10226  iseqf1olemqcl  10227  iseqf1olemnab  10229  iseqf1olemmo  10233  iseqf1olemqk  10235  iseqf1olemjpcl  10236  iseqf1olemfvp  10238  seq3f1olemqsumkj  10239  seq3f1olemqsumk  10240  seq3f1olemqsum  10241  seq3f1olemstep  10242  seq3f1olemp  10243  seq3f1oleml  10244  seq3f1o  10245  hashfz1  10497  omgadd  10516  hashfacen  10547  leisorel  10548  zfz1isolemiso  10550  seq3coll  10553  cnrecnv  10650  sumeq2  11096  summodclem3  11117  summodclem2a  11118  fsumgcl  11123  fsum3  11124  fsumf1o  11127  fisumss  11129  fsumcl2lem  11135  fsumadd  11143  fsummulc2  11185  sqpweven  11780  2sqpwodd  11781  phimullem  11828  ennnfonelemjn  11842  ennnfonelemp1  11846  ennnfonelemhdmp1  11849  ennnfonelemss  11850  ennnfonelemkh  11852  ennnfonelemhf1o  11853  ennnfonelemex  11854  ennnfonelemnn0  11862  ennnfonelemim  11864  ctinfomlemom  11867  ctiunctlemudc  11877  ctiunctlemfo  11879  ssidcn  12306  txhmeo  12415  dvid  12758  dvexp  12771  isomninnlem  13152
  Copyright terms: Public domain W3C validator