Metamath Proof Explorer

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 
|- Pg = setrecs ( ( x e. _V |-> ( ~P x X. ~P x ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpg 
 |-  Pg
1 vx 
 |-  x
2 cvv 
 |-  _V
3 1 cv 
 |-  x
4 3 cpw 
 |-  ~P x
5 4 4 cxp 
 |-  ( ~P x X. ~P x )
6 1 2 5 cmpt 
 |-  ( x e. _V |-> ( ~P x X. ~P x ) )
7 6 csetrecs 
 |-  setrecs ( ( x e. _V |-> ( ~P x X. ~P x ) ) )
8 0 7 wceq 
 |-  Pg = setrecs ( ( x e. _V |-> ( ~P x X. ~P x ) ) )