Nearby theorems
|
|
New Foundations Explorer |
< Previous
Next >
Nearby theorems |
|
| Mirrors > Home > NFE Home > Th. List > df-ins4 | Unicode version | ||
| Description: Define the fourth insertion operation. (Contributed by SF, 9-Feb-2015.) |
| Ref | Expression |
|---|---|
| df-ins4 |
 Ins4         
 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cA |
. . 3
 | |
| 2 | 1 | cins4 5755 |
. 2
Ins4 |
| 3 | c1st 4717 |
. . . . 5
| |
| 4 | c2nd 4783 |
. . . . . . 7
| |
| 5 | 3, 4 | ccom 4721 |
. . . . . 6
|
| 6 | 5, 4 | ccom 4721 |
. . . . . 6
|
| 7 | 5, 6 | ctxp 5735 |
. . . . 5
|
| 8 | 3, 7 | ctxp 5735 |
. . . 4
|
| 9 | 8 | ccnv 4771 |
. . 3
|
| 10 | 9, 1 | cima 4722 |
. 2
|
| 11 | 2, 10 | wceq 1642 |
1
 Ins4
|
| Colors of variables: wff setvar class |
| This definition is referenced by: oqelins4 5794 ins4ex 5799 |
| Copyright terms: Public domain | W3C validator |