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

Definition df-f1 5240
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 5232 . 2  wff  F : A -1-1-> B
51, 2, 3wf 5231 . . 3  wff  F : A
--> B
63ccnv 4643 . . . 4  class  `' F
76wfun 5229 . . 3  wff  Fun  `' F
85, 7wa 104 . 2  wff  ( F : A --> B  /\  Fun  `' F )
94, 8wb 105 1  wff  ( F : A -1-1-> B  <->  ( F : A --> B  /\  Fun  `' F ) )
Colors of variables: wff set class
This definition is referenced by:  f1eq1  5435  f1eq2  5436  f1eq3  5437  nff1  5438  dff12  5439  f1f  5440  f1ss  5446  f1ssr  5447  f1ssres  5449  f1cnvcnv  5451  f1co  5452  dff1o2  5485  f1f1orn  5491  f1imacnv  5497  fun11iun  5501  f11o  5513  f10  5514  f1o2ndf1  6252  ssdomg  6803  phplem4dom  6889  sbthlemi9  6993  casefun  7113  casef1  7118  djufun  7132  exmidfodomrlemim  7229  4sqlemffi  12427  ennnfonelemf1  12468
  Copyright terms: Public domain W3C validator