Definition df-p6 4192

Description: Define the P6 operator. This is the set guaranteed by ax-typlower 4087. (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

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	cp6 4179	. 2 class P6 A
3		cvv 2860	. . . . 5 class V
4		vx	. . . . . . . 8 setvar x
5	4	cv 1641	. . . . . . 7 class x
6	5	csn 3738	. . . . . 6 class {x}
7	6	csn 3738	. . . . 5 class {{x}}
8	3, 7	cxpk 4175	. . . 4 class (V ×k {{x}})
9	8, 1	wss 3258	. . 3 wff (V ×k {{x}}) ⊆ A
10	9, 4	cab 2339	. 2 class {x ∣ (V ×k {{x}}) ⊆ A}
11	2, 10	wceq 1642	1 wff P6 A = {x ∣ (V ×k {{x}}) ⊆ A}

This definition is referenced by:  p6eq  4239  elp6  4264