Definition df-ins4 5757

Description: Define the fourth insertion operation. (Contributed by SF, 9-Feb-2015.)

Assertion

Ref	Expression
df-ins4	|- Ins4 A = (`'(1st (x) ((1st o. 2nd) (x) ((1st o. 2nd) o. 2nd)))"A)

Detailed syntax breakdown of Definition df-ins4

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	cins4 5756	. 2 class Ins4 A
3		c1st 4718	. . . . 5 class 1st
4		c2nd 4784	. . . . . . 7 class 2nd
5	3, 4	ccom 4722	. . . . . 6 class (1st o. 2nd)
6	5, 4	ccom 4722	. . . . . 6 class ((1st o. 2nd) o. 2nd)
7	5, 6	ctxp 5736	. . . . 5 class ((1st o. 2nd) (x) ((1st o. 2nd) o. 2nd))
8	3, 7	ctxp 5736	. . . 4 class (1st (x) ((1st o. 2nd) (x) ((1st o. 2nd) o. 2nd)))
9	8	ccnv 4772	. . 3 class `'(1st (x) ((1st o. 2nd) (x) ((1st o. 2nd) o. 2nd)))
10	9, 1	cima 4723	. 2 class (`'(1st (x) ((1st o. 2nd) (x) ((1st o. 2nd) o. 2nd)))"A)
11	2, 10	wceq 1642	1 wff Ins4 A = (`'(1st (x) ((1st o. 2nd) (x) ((1st o. 2nd) o. 2nd)))"A)

This definition is referenced by:  oqelins4  5795  ins4ex  5800