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

Definition df-imagek 4194
Description: Define the Kuratowski image function. See opkelimagek 4272 for membership. (Contributed by SF, 12-Jan-2015.)
Assertion
Ref Expression
df-imagek Imagek k Ins2k Sk Ins3k Sk k k SIk k1 1 1c

Detailed syntax breakdown of Definition df-imagek
StepHypRef Expression
1 cA . . 3
21cimagek 4182 . 2 Imagek
3 cvv 2859 . . . 4
43, 3cxpk 4174 . . 3 k
5 cssetk 4183 . . . . . 6 Sk
65cins2k 4176 . . . . 5 Ins2k Sk
71csik 4181 . . . . . . . 8 SIk
87ccnvk 4175 . . . . . . 7 k SIk
95, 8ccomk 4180 . . . . . 6 Sk k k SIk
109cins3k 4177 . . . . 5 Ins3k Sk k k SIk
116, 10csymdif 3209 . . . 4 Ins2k Sk Ins3k Sk k k SIk
12 c1c 4134 . . . . . 6 1c
1312cpw1 4135 . . . . 5 1 1c
1413cpw1 4135 . . . 4 1 1 1c
1511, 14cimak 4179 . . 3 Ins2k Sk Ins3k Sk k k SIk k1 1 1c
164, 15cdif 3206 . 2 k Ins2k Sk Ins3k Sk k k SIk k1 1 1c
172, 16wceq 1642 1 Imagek k Ins2k Sk Ins3k Sk k k SIk k1 1 1c
Colors of variables: wff setvar class
This definition is referenced by:  imagekeq  4244  opkelimagekg  4271  imagekrelk  4273  imagekexg  4311
  Copyright terms: Public domain W3C validator