Definition df-ima 4728

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 4723	. 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 4640	. . . 4 wff yAx
9	8, 4, 2	wrex 2616	. . 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  4746  elima  4755  imaeq1  4938  imaeq2  4939  dfima4  4953  nfima  4954  imadmrn  5009  imasn  5019  dfimafn  5367  isoini  5498  clos1basesuc  5883  enpw1pw  6076