Nearby theorems
|
|
New Foundations Explorer |
< Previous
Next >
Nearby theorems |
|
| Mirrors > Home > NFE Home > Th. List > df-ins2 | Unicode version | ||
| Description: Define the second insertion operation. (Contributed by SF, 9-Feb-2015.) |
| Ref | Expression |
|---|---|
| df-ins2 |
 Ins2       |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cA |
. . 3
 | |
| 2 | 1 | cins2 5750 |
. 2
Ins2 |
| 3 | cvv 2860 |
. . 3
| |
| 4 | 3, 1 | ctxp 5736 |
. 2
|
| 5 | 2, 4 | wceq 1642 |
1
 Ins2 |
| Colors of variables: wff setvar class |
| This definition is referenced by: otelins2 5792 ins2exg 5796 |
| Copyright terms: Public domain | W3C validator |