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

Definition df-imak 4189
Description: Define the Kuratowski image operator. (Contributed by SF, 12-Jan-2015.)
Assertion
Ref Expression
df-imak k
Distinct variable groups:   ,,   ,,

Detailed syntax breakdown of Definition df-imak
StepHypRef Expression
1 cA . . 3
2 cB . . 3
31, 2cimak 4179 . 2 k
4 vy . . . . . . 7
54cv 1641 . . . . . 6
6 vx . . . . . . 7
76cv 1641 . . . . . 6
85, 7copk 4057 . . . . 5
98, 1wcel 1710 . . . 4
109, 4, 2wrex 2615 . . 3
1110, 6cab 2339 . 2
123, 11wceq 1642 1 k
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