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

Theorem f1of 5157
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 5156 . 2  |-  ( F : A -1-1-onto-> B  ->  F : A -1-1-> B )
2 f1f 5123 . 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 4928   -1-1->wf1 4929   -1-1-onto->wf1o 4931
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 4937  df-f1o 4939
This theorem is referenced by:  f1ofn  5158  f1oabexg  5169  f1ompt  5352  f1oresrab  5361  fsn  5367  fsnunf  5394  f1ocnvfv1  5448  f1ocnvfv2  5449  f1ocnvdm  5452  fcof1o  5460  isocnv  5482  isores2  5484  isotr  5487  isopolem  5492  isosolem  5494  f1oiso2  5497  f1ofveu  5531  smoiso  5951  f1oen2g  6302  en1  6346  enm  6364  fidceq  6404  dif1en  6414  fin0  6419  fin0or  6420  ac6sfi  6431  en2eqpr  6434  isotilem  6478  supisoex  6481  supisoti  6482  ordiso2  6505  frecuzrdgg  9498  sizefz1  9807  omgadd  9826  cnrecnv  9935  sumeq2d  10334  sumeq2  10335  sqpweven  10697  2sqpwodd  10698
  Copyright terms: Public domain W3C validator