Definition df-imak 4190

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

Assertion

Ref	Expression
df-imak	⊢ (A “k B) = {x ∣ ∃y ∈ B ⟪y, x⟫ ∈ 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 “k B)
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⟫ ∈ A
10	9, 4, 2	wrex 2616	. . 3 wff ∃y ∈ B ⟪y, x⟫ ∈ A
11	10, 6	cab 2339	. 2 class {x ∣ ∃y ∈ B ⟪y, x⟫ ∈ A}
12	3, 11	wceq 1642	1 wff (A “k B) = {x ∣ ∃y ∈ B ⟪y, x⟫ ∈ A}

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