NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-p6 GIF 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 A = {x (V ×k {{x}}) A}
Distinct variable group:   x,A

Detailed syntax breakdown of Definition df-p6
StepHypRef Expression
1 cA . . 3 class A
21cp6 4178 . 2 class P6 A
3 cvv 2859 . . . . 5 class V
4 vx . . . . . . . 8 setvar x
54cv 1641 . . . . . . 7 class x
65csn 3737 . . . . . 6 class {x}
76csn 3737 . . . . 5 class {{x}}
83, 7cxpk 4174 . . . 4 class (V ×k {{x}})
98, 1wss 3257 . . 3 wff (V ×k {{x}}) A
109, 4cab 2339 . 2 class {x (V ×k {{x}}) A}
112, 10wceq 1642 1 wff P6 A = {x (V ×k {{x}}) A}
Colors of variables: wff setvar class
This definition is referenced by:  p6eq  4238  elp6  4263
  Copyright terms: Public domain W3C validator