NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-cok GIF version

Definition df-cok 4190
Description: Define the Kuratowski composition operator. (Contributed by SF, 12-Jan-2015.)
Assertion
Ref Expression
df-cok (A k B) = (( Ins2k AIns3k kB) “k V)

Detailed syntax breakdown of Definition df-cok
StepHypRef Expression
1 cA . . 3 class A
2 cB . . 3 class B
31, 2ccomk 4180 . 2 class (A k B)
41cins2k 4176 . . . 4 class Ins2k A
52ccnvk 4175 . . . . 5 class kB
65cins3k 4177 . . . 4 class Ins3k kB
74, 6cin 3208 . . 3 class ( Ins2k AIns3k kB)
8 cvv 2859 . . 3 class V
97, 8cimak 4179 . 2 class (( Ins2k AIns3k kB) “k V)
103, 9wceq 1642 1 wff (A k B) = (( Ins2k AIns3k kB) “k V)
Colors of variables: wff setvar class
This definition is referenced by:  cokeq1  4230  cokeq2  4231  opkelcokg  4261  cokrelk  4284  cokexg  4309
  Copyright terms: Public domain W3C validator