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

Definition df-ins4 5756
Description: Define the fourth insertion operation. (Contributed by SF, 9-Feb-2015.)
Assertion
Ref Expression
df-ins4 Ins4 A = ((1st ⊗ ((1st 2nd ) ⊗ ((1st 2nd ) 2nd ))) “ A)

Detailed syntax breakdown of Definition df-ins4
StepHypRef Expression
1 cA . . 3 class A
21cins4 5755 . 2 class Ins4 A
3 c1st 4717 . . . . 5 class 1st
4 c2nd 4783 . . . . . . 7 class 2nd
53, 4ccom 4721 . . . . . 6 class (1st 2nd )
65, 4ccom 4721 . . . . . 6 class ((1st 2nd ) 2nd )
75, 6ctxp 5735 . . . . 5 class ((1st 2nd ) ⊗ ((1st 2nd ) 2nd ))
83, 7ctxp 5735 . . . 4 class (1st ⊗ ((1st 2nd ) ⊗ ((1st 2nd ) 2nd )))
98ccnv 4771 . . 3 class (1st ⊗ ((1st 2nd ) ⊗ ((1st 2nd ) 2nd )))
109, 1cima 4722 . 2 class ((1st ⊗ ((1st 2nd ) ⊗ ((1st 2nd ) 2nd ))) “ A)
112, 10wceq 1642 1 wff Ins4 A = ((1st ⊗ ((1st 2nd ) ⊗ ((1st 2nd ) 2nd ))) “ A)
Colors of variables: wff setvar class
This definition is referenced by:  oqelins4  5794  ins4ex  5799
  Copyright terms: Public domain W3C validator