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

Definition df-f1 5201
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 5193 . 2  wff  F : A -1-1-> B
51, 2, 3wf 5192 . . 3  wff  F : A
--> B
63ccnv 4608 . . . 4  class  `' F
76wfun 5190 . . 3  wff  Fun  `' F
85, 7wa 103 . 2  wff  ( F : A --> B  /\  Fun  `' F )
94, 8wb 104 1  wff  ( F : A -1-1-> B  <->  ( F : A --> B  /\  Fun  `' F ) )
Colors of variables: wff set class
This definition is referenced by:  f1eq1  5396  f1eq2  5397  f1eq3  5398  nff1  5399  dff12  5400  f1f  5401  f1ss  5407  f1ssr  5408  f1ssres  5410  f1cnvcnv  5412  f1co  5413  dff1o2  5445  f1f1orn  5451  f1imacnv  5457  fun11iun  5461  f11o  5473  f10  5474  f1o2ndf1  6205  ssdomg  6754  phplem4dom  6838  sbthlemi9  6940  casefun  7060  casef1  7065  djufun  7079  exmidfodomrlemim  7171  ennnfonelemf1  12366
  Copyright terms: Public domain W3C validator