Definition df-pg

Description: Define the class of partisan games. More precisely, this is the class of partisan game forms, many of which represent equal partisan games. In Metamath, equality between partisan games is represented by a different equivalence relation than class equality. (Contributed by Emmett Weisz, 22-Aug-2021)

	Ref	Expression
Assertion	df-pg	$$⊢\mathrm{Pg}=\mathrm{setrecs}\left(\left(x\in \mathrm{V}⟼𝒫x\times 𝒫x\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpg	$$class\mathrm{Pg}$$
1		vx	$$setvarx$$
2		cvv	$$class\mathrm{V}$$
3	1	cv	$$setvarx$$
4	3	cpw	$$class𝒫x$$
5	4 4	cxp	$$class\left(𝒫x\times 𝒫x\right)$$
6	1 2 5	cmpt	$$class\left(x\in \mathrm{V}⟼𝒫x\times 𝒫x\right)$$
7	6	csetrecs	$$class\mathrm{setrecs}\left(\left(x\in \mathrm{V}⟼𝒫x\times 𝒫x\right)\right)$$
8	0 7	wceq	$$wff\mathrm{Pg}=\mathrm{setrecs}\left(\left(x\in \mathrm{V}⟼𝒫x\times 𝒫x\right)\right)$$