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

Definition df-f1 4934
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 4926 . 2  wff  F : A -1-1-> B
51, 2, 3wf 4925 . . 3  wff  F : A
--> B
63ccnv 4371 . . . 4  class  `' F
76wfun 4923 . . 3  wff  Fun  `' F
85, 7wa 101 . 2  wff  ( F : A --> B  /\  Fun  `' F )
94, 8wb 102 1  wff  ( F : A -1-1-> B  <->  ( F : A --> B  /\  Fun  `' F ) )
Colors of variables: wff set class
This definition is referenced by:  f1eq1  5114  f1eq2  5115  f1eq3  5116  nff1  5117  dff12  5118  f1f  5119  f1ss  5124  f1ssr  5125  f1ssres  5126  f1cnvcnv  5127  f1co  5128  dff1o2  5158  f1f1orn  5164  f1imacnv  5170  fun11iun  5174  f11o  5186  f10  5187  f1o2ndf1  5876  ssdomg  6288  phplem4dom  6354
  Copyright terms: Public domain W3C validator