Definition df-image 5755

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 ∘ ◡ SI A)) “ 1c)

Detailed syntax breakdown of Definition df-image

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	cimage 5754	. 2 class ImageA
3		csset 4720	. . . . . 6 class S
4	3	cins2 5750	. . . . 5 class Ins2 S
5	1	csi 4721	. . . . . . . 8 class SI A
6	5	ccnv 4772	. . . . . . 7 class ◡ SI A
7	3, 6	ccom 4722	. . . . . 6 class ( S ∘ ◡ SI A)
8	7	cins3 5752	. . . . 5 class Ins3 ( S ∘ ◡ SI A)
9	4, 8	csymdif 3210	. . . 4 class ( Ins2 S ⊕ Ins3 ( S ∘ ◡ SI A))
10		c1c 4135	. . . 4 class 1c
11	9, 10	cima 4723	. . 3 class (( Ins2 S ⊕ Ins3 ( S ∘ ◡ SI A)) “ 1c)
12	11	ccompl 3206	. 2 class ∼ (( Ins2 S ⊕ Ins3 ( S ∘ ◡ SI A)) “ 1c)
13	2, 12	wceq 1642	1 wff ImageA = ∼ (( Ins2 S ⊕ Ins3 ( S ∘ ◡ SI A)) “ 1c)

This definition is referenced by:  brimage  5794  imageexg  5801