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

Theorem f1f 5440
Description: A one-to-one mapping is a mapping. (Contributed by NM, 31-Dec-1996.)
Assertion
Ref Expression
f1f  |-  ( F : A -1-1-> B  ->  F : A --> B )

Proof of Theorem f1f
StepHypRef Expression
1 df-f1 5240 . 2  |-  ( F : A -1-1-> B  <->  ( F : A --> B  /\  Fun  `' F ) )
21simplbi 274 1  |-  ( F : A -1-1-> B  ->  F : A --> B )
Colors of variables: wff set class
Syntax hints:    -> wi 4   `'ccnv 4643   Fun wfun 5229   -->wf 5231   -1-1->wf1 5232
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106
This theorem depends on definitions:  df-bi 117  df-f1 5240
This theorem is referenced by:  f1rn  5441  f1fn  5442  f1ss  5446  f1ssres  5449  f1of  5480  dff1o5  5489  fsnd  5523  cocan1  5809  f1o2ndf1  6254  brdomg  6775  f1dom2g  6783  f1domg  6785  dom3d  6801  f1imaen2g  6820  2dom  6832  xpdom2  6858  dom0  6867  phplem4dom  6891  isinfinf  6926  infm  6933  updjudhcoinlf  7110  updjudhcoinrg  7111  casef1  7120  djudom  7123  difinfsnlem  7129  difinfsn  7130  fihashf1rn  10803  ennnfonelemrn  12473  reeff1o  14671  1dom1el  15221  pwle2  15227
  Copyright terms: Public domain W3C validator