df-ima - New Foundations Explorer

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

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}

Colors of variables: wff setvar class

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