Definition df-image 5754

Description: Define the image function of a class. (Contributed by SF, 9-Feb-2015.) (Revised by Scott Fenton, 19-Apr-2021.)

Assertion

Ref	Expression
df-image	|- ImageA = ∼ (( Ins2 S (+) Ins3 ( S o. `' SI A))"1c)

Detailed syntax breakdown of Definition df-image

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	cimage 5753	. 2 class ImageA
3		csset 4719	. . . . . 6 class S
4	3	cins2 5749	. . . . 5 class Ins2 S
5	1	csi 4720	. . . . . . . 8 class SI A
6	5	ccnv 4771	. . . . . . 7 class `' SI A
7	3, 6	ccom 4721	. . . . . 6 class ( S o. `' SI A)
8	7	cins3 5751	. . . . 5 class Ins3 ( S o. `' SI A)
9	4, 8	csymdif 3209	. . . 4 class ( Ins2 S (+) Ins3 ( S o. `' SI A))
10		c1c 4134	. . . 4 class 1c
11	9, 10	cima 4722	. . 3 class (( Ins2 S (+) Ins3 ( S o. `' SI A))"1c)
12	11	ccompl 3205	. 2 class ∼ (( Ins2 S (+) Ins3 ( S o. `' SI A))"1c)
13	2, 12	wceq 1642	1 wff ImageA = ∼ (( Ins2 S (+) Ins3 ( S o. `' SI A))"1c)

This definition is referenced by:  brimage  5793  imageexg  5800