New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > df-p6 | Unicode version |
Description: Define the P6 operator. This is the set guaranteed by ax-typlower 4086. (Contributed by SF, 12-Jan-2015.) |
Ref | Expression |
---|---|
df-p6 | P6 k |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 | |
2 | 1 | cp6 4178 | . 2 P6 |
3 | cvv 2859 | . . . . 5 | |
4 | vx | . . . . . . . 8 | |
5 | 4 | cv 1641 | . . . . . . 7 |
6 | 5 | csn 3737 | . . . . . 6 |
7 | 6 | csn 3737 | . . . . 5 |
8 | 3, 7 | cxpk 4174 | . . . 4 k |
9 | 8, 1 | wss 3257 | . . 3 k |
10 | 9, 4 | cab 2339 | . 2 k |
11 | 2, 10 | wceq 1642 | 1 P6 k |
Colors of variables: wff setvar class |
This definition is referenced by: p6eq 4238 elp6 4263 |
Copyright terms: Public domain | W3C validator |