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

Definition df-p6 4191
Description: Define the P6 operator. This is the set guaranteed by ax-typlower 4086. (Contributed by SF, 12-Jan-2015.)
Assertion
Ref Expression
df-p6 P6 k
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-p6
StepHypRef Expression
1 cA . . 3
21cp6 4178 . 2 P6
3 cvv 2859 . . . . 5
4 vx . . . . . . . 8
54cv 1641 . . . . . . 7
65csn 3737 . . . . . 6
76csn 3737 . . . . 5
83, 7cxpk 4174 . . . 4 k
98, 1wss 3257 . . 3 k
109, 4cab 2339 . 2 k
112, 10wceq 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