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

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

Detailed syntax breakdown of Definition df-image
StepHypRef Expression
1 cA . . 3 class A
21cimage 5753 . 2 class ImageA
3 csset 4719 . . . . . 6 class S
43cins2 5749 . . . . 5 class Ins2 S
51csi 4720 . . . . . . . 8 class SI A
65ccnv 4771 . . . . . . 7 class SI A
73, 6ccom 4721 . . . . . 6 class ( S SI A)
87cins3 5751 . . . . 5 class Ins3 ( S SI A)
94, 8csymdif 3209 . . . 4 class ( Ins2 S Ins3 ( S SI A))
10 c1c 4134 . . . 4 class 1c
119, 10cima 4722 . . 3 class (( Ins2 S Ins3 ( S SI A)) “ 1c)
1211ccompl 3205 . 2 class ∼ (( Ins2 S Ins3 ( S SI A)) “ 1c)
132, 12wceq 1642 1 wff ImageA = ∼ (( Ins2 S Ins3 ( S SI A)) “ 1c)
Colors of variables: wff setvar class
This definition is referenced by:  brimage  5793  imageexg  5800
  Copyright terms: Public domain W3C validator