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

Definition df-f1 4977
Description: Define a one-to-one function. Compare Definition 6.15(5) of [TakeutiZaring] p. 27. We use their notation ("1-1" above the arrow). (Contributed by NM, 1-Aug-1994.)
Assertion
Ref Expression
df-f1  |-  ( F : A -1-1-> B  <->  ( F : A --> B  /\  Fun  `' F ) )

Detailed syntax breakdown of Definition df-f1
StepHypRef Expression
1 cA . . 3  class  A
2 cB . . 3  class  B
3 cF . . 3  class  F
41, 2, 3wf1 4969 . 2  wff  F : A -1-1-> B
51, 2, 3wf 4968 . . 3  wff  F : A
--> B
63ccnv 4403 . . . 4  class  `' F
76wfun 4966 . . 3  wff  Fun  `' F
85, 7wa 102 . 2  wff  ( F : A --> B  /\  Fun  `' F )
94, 8wb 103 1  wff  ( F : A -1-1-> B  <->  ( F : A --> B  /\  Fun  `' F ) )
Colors of variables: wff set class
This definition is referenced by:  f1eq1  5162  f1eq2  5163  f1eq3  5164  nff1  5165  dff12  5166  f1f  5167  f1ss  5173  f1ssr  5174  f1ssres  5176  f1cnvcnv  5178  f1co  5179  dff1o2  5209  f1f1orn  5215  f1imacnv  5221  fun11iun  5225  f11o  5237  f10  5238  f1o2ndf1  5931  ssdomg  6428  phplem4dom  6511  sbthlemi9  6595  casefun  6697  casef1  6702  djufun  6705  exmidfodomrlemim  6748
  Copyright terms: Public domain W3C validator