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

Definition df-imak 4189
Description: Define the Kuratowski image operator. (Contributed by SF, 12-Jan-2015.)
Assertion
Ref Expression
df-imak (Ak B) = {x y By, x A}
Distinct variable groups:   x,A,y   x,B,y

Detailed syntax breakdown of Definition df-imak
StepHypRef Expression
1 cA . . 3 class A
2 cB . . 3 class B
31, 2cimak 4179 . 2 class (Ak B)
4 vy . . . . . . 7 setvar y
54cv 1641 . . . . . 6 class y
6 vx . . . . . . 7 setvar x
76cv 1641 . . . . . 6 class x
85, 7copk 4057 . . . . 5 class y, x
98, 1wcel 1710 . . . 4 wff y, x A
109, 4, 2wrex 2615 . . 3 wff y By, x A
1110, 6cab 2339 . 2 class {x y By, x A}
123, 11wceq 1642 1 wff (Ak B) = {x y By, x A}
Colors of variables: wff setvar class
This definition is referenced by:  imakeq1  4224  imakeq2  4225  elimakg  4257  setswith  4321
  Copyright terms: Public domain W3C validator