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

Definition df-f1 4885
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 4877 . 2  wff  F : A -1-1-> B
51, 2, 3wf 4876 . . 3  wff  F : A
--> B
63ccnv 4322 . . . 4  class  `' F
76wfun 4874 . . 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  5065  f1eq2  5066  f1eq3  5067  nff1  5068  dff12  5069  f1f  5070  f1ss  5075  f1ssr  5076  f1ssres  5077  f1cnvcnv  5078  f1co  5079  dff1o2  5109  f1f1orn  5115  f1imacnv  5121  fun11iun  5125  f11o  5137  f10  5138  f1o2ndf1  5827  ssdomg  6236  phplem4dom  6302
  Copyright terms: Public domain W3C validator