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

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

Proof of Theorem f1f
StepHypRef Expression
1 df-f1 4850 . 2  F : -1-1->  F : -->  Fun  `' F
21simplbi 259 1  F : -1-1->  F : -->
Colors of variables: wff set class
Syntax hints:   wi 4   `'ccnv 4287   Fun wfun 4839   -->wf 4841   -1-1->wf1 4842
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99
This theorem depends on definitions:  df-bi 110  df-f1 4850
This theorem is referenced by:  f1fn  5036  f1ss  5040  f1ssres  5042  f1of  5069  dff1o5  5078  fun11iun  5090  cocan1  5370  f1dmex  5685  f1o2ndf1  5791  brdomg  6165  f1dom2g  6172  f1domg  6174  dom3d  6190  f1imaen2g  6209  2dom  6221  xpdom2  6241
  Copyright terms: Public domain W3C validator