Definition df-si3 5759

Description: Define the triple singleton image. (Contributed by SF, 9-Feb-2015.)

Assertion

Ref	Expression
df-si3	|- SI3 A = (( SI 1st (x) ( SI (1st o. 2nd) (x) SI (2nd o. 2nd)))"~P1 A)

Detailed syntax breakdown of Definition df-si3

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	csi3 5758	. 2 class SI3 A
3		c1st 4718	. . . . 5 class 1st
4	3	csi 4721	. . . 4 class SI 1st
5		c2nd 4784	. . . . . . 7 class 2nd
6	3, 5	ccom 4722	. . . . . 6 class (1st o. 2nd)
7	6	csi 4721	. . . . 5 class SI (1st o. 2nd)
8	5, 5	ccom 4722	. . . . . 6 class (2nd o. 2nd)
9	8	csi 4721	. . . . 5 class SI (2nd o. 2nd)
10	7, 9	ctxp 5736	. . . 4 class ( SI (1st o. 2nd) (x) SI (2nd o. 2nd))
11	4, 10	ctxp 5736	. . 3 class ( SI 1st (x) ( SI (1st o. 2nd) (x) SI (2nd o. 2nd)))
12	1	cpw1 4136	. . 3 class ~P1 A
13	11, 12	cima 4723	. 2 class (( SI 1st (x) ( SI (1st o. 2nd) (x) SI (2nd o. 2nd)))"~P1 A)
14	2, 13	wceq 1642	1 wff SI3 A = (( SI 1st (x) ( SI (1st o. 2nd) (x) SI (2nd o. 2nd)))"~P1 A)

This definition is referenced by:  otsnelsi3  5806  si3ex  5807