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

Definition df-f1 5203
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 5195 . 2  wff  F : A -1-1-> B
51, 2, 3wf 5194 . . 3  wff  F : A
--> B
63ccnv 4610 . . . 4  class  `' F
76wfun 5192 . . 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  5398  f1eq2  5399  f1eq3  5400  nff1  5401  dff12  5402  f1f  5403  f1ss  5409  f1ssr  5410  f1ssres  5412  f1cnvcnv  5414  f1co  5415  dff1o2  5447  f1f1orn  5453  f1imacnv  5459  fun11iun  5463  f11o  5475  f10  5476  f1o2ndf1  6207  ssdomg  6756  phplem4dom  6840  sbthlemi9  6942  casefun  7062  casef1  7067  djufun  7081  exmidfodomrlemim  7178  ennnfonelemf1  12373
  Copyright terms: Public domain W3C validator