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

Definition df-f1 5084
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 5076 . 2  wff  F : A -1-1-> B
51, 2, 3wf 5075 . . 3  wff  F : A
--> B
63ccnv 4496 . . . 4  class  `' F
76wfun 5073 . . 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  5279  f1eq2  5280  f1eq3  5281  nff1  5282  dff12  5283  f1f  5284  f1ss  5290  f1ssr  5291  f1ssres  5293  f1cnvcnv  5295  f1co  5296  dff1o2  5326  f1f1orn  5332  f1imacnv  5338  fun11iun  5342  f11o  5354  f10  5355  f1o2ndf1  6077  ssdomg  6624  phplem4dom  6707  sbthlemi9  6803  casefun  6920  casef1  6925  djufun  6939  exmidfodomrlemim  7002  ennnfonelemf1  11770
  Copyright terms: Public domain W3C validator