Definition df-ima 4727

Description: Define the image of one class under another. (Contributed by SF, 5-Jan-2015.)

Assertion

Ref	Expression
df-ima	⊢ (A “ B) = {x ∣ ∃y ∈ B yAx}

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

Detailed syntax breakdown of Definition df-ima

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3	1, 2	cima 4722	. 2 class (A “ B)
4		vy	. . . . . 6 setvar y
5	4	cv 1641	. . . . 5 class y
6		vx	. . . . . 6 setvar x
7	6	cv 1641	. . . . 5 class x
8	5, 7, 1	wbr 4639	. . . 4 wff yAx
9	8, 4, 2	wrex 2615	. . 3 wff ∃y ∈ B yAx
10	9, 6	cab 2339	. 2 class {x ∣ ∃y ∈ B yAx}
11	3, 10	wceq 1642	1 wff (A “ B) = {x ∣ ∃y ∈ B yAx}

This definition is referenced by:  dfima2  4745  elima  4754  imaeq1  4937  imaeq2  4938  dfima4  4952  nfima  4953  imadmrn  5008  imasn  5018  dfimafn  5366  isoini  5497  clos1basesuc  5882  enpw1pw  6075