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

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

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