Definition df-imak 4190

Description: Define the Kuratowski image operator. (Contributed by SF, 12-Jan-2015.)

Assertion

Ref	Expression
df-imak	|- (A"kB) = {x | E.y e. B <<y, x>> e. A}

Distinct variable groups:   x,A,y   x,B,y

Detailed syntax breakdown of Definition df-imak

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3	1, 2	cimak 4180	. 2 class (A"kB)
4		vy	. . . . . . 7 setvar y
5	4	cv 1641	. . . . . 6 class y
6		vx	. . . . . . 7 setvar x
7	6	cv 1641	. . . . . 6 class x
8	5, 7	copk 4058	. . . . 5 class <<y, x>>
9	8, 1	wcel 1710	. . . 4 wff <<y, x>> e. A
10	9, 4, 2	wrex 2616	. . 3 wff E.y e. B <<y, x>> e. A
11	10, 6	cab 2339	. 2 class {x | E.y e. B <<y, x>> e. A}
12	3, 11	wceq 1642	1 wff (A"kB) = {x | E.y e. B <<y, x>> e. A}

This definition is referenced by:  imakeq1  4225  imakeq2  4226  elimakg  4258  setswith  4322