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

Definition df-f1 4907
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 4899 . 2  wff  F : A -1-1-> B
51, 2, 3wf 4898 . . 3  wff  F : A
--> B
63ccnv 4344 . . . 4  class  `' F
76wfun 4896 . . 3  wff  Fun  `' F
85, 7wa 97 . 2  wff  ( F : A --> B  /\  Fun  `' F )
94, 8wb 98 1  wff  ( F : A -1-1-> B  <->  ( F : A --> B  /\  Fun  `' F ) )
Colors of variables: wff set class
This definition is referenced by:  f1eq1  5087  f1eq2  5088  f1eq3  5089  nff1  5090  dff12  5091  f1f  5092  f1ss  5097  f1ssr  5098  f1ssres  5099  f1cnvcnv  5100  f1co  5101  dff1o2  5131  f1f1orn  5137  f1imacnv  5143  fun11iun  5147  f11o  5159  f10  5160  f1o2ndf1  5849  ssdomg  6258  phplem4dom  6324
  Copyright terms: Public domain W3C validator