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

Definition df-f1 4988
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 4980 . 2  wff  F : A -1-1-> B
51, 2, 3wf 4979 . . 3  wff  F : A
--> B
63ccnv 4412 . . . 4  class  `' F
76wfun 4977 . . 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  5176  f1eq2  5177  f1eq3  5178  nff1  5179  dff12  5180  f1f  5181  f1ss  5187  f1ssr  5188  f1ssres  5190  f1cnvcnv  5192  f1co  5193  dff1o2  5223  f1f1orn  5229  f1imacnv  5235  fun11iun  5239  f11o  5251  f10  5252  f1o2ndf1  5952  ssdomg  6449  phplem4dom  6532  sbthlemi9  6621  casefun  6723  casef1  6728  djufun  6731  exmidfodomrlemim  6774
  Copyright terms: Public domain W3C validator