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

Definition df-si3 5758
Description: Define the triple singleton image. (Contributed by SF, 9-Feb-2015.)
Assertion
Ref Expression
df-si3 SI3 SI SI SI 1

Detailed syntax breakdown of Definition df-si3
StepHypRef Expression
1 cA . . 3
21csi3 5757 . 2 SI3
3 c1st 4717 . . . . 5
43csi 4720 . . . 4 SI
5 c2nd 4783 . . . . . . 7
63, 5ccom 4721 . . . . . 6
76csi 4720 . . . . 5 SI
85, 5ccom 4721 . . . . . 6
98csi 4720 . . . . 5 SI
107, 9ctxp 5735 . . . 4 SI SI
114, 10ctxp 5735 . . 3 SI SI SI
121cpw1 4135 . . 3 1
1311, 12cima 4722 . 2 SI SI SI 1
142, 13wceq 1642 1 SI3 SI SI SI 1
Colors of variables: wff setvar class
This definition is referenced by:  otsnelsi3  5805  si3ex  5806
  Copyright terms: Public domain W3C validator