NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-image Unicode 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 Image Ins2 S Ins3 S SI 1c

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