Metamath Proof Explorer


Definition df-goel

Description: Define the Godel-set of membership. Here the arguments x = <. N , P >. correspond to v_N and v_P , so ( (/) e.g 1o ) actually means v_0 e. v_1 , not 0 e. 1 . (Contributed by Mario Carneiro, 14-Jul-2013)

Ref Expression
Assertion df-goel 𝑔 = x ω × ω x

Detailed syntax breakdown

Step Hyp Ref Expression
0 cgoe class 𝑔
1 vx setvar x
2 com class ω
3 2 2 cxp class ω × ω
4 c0 class
5 1 cv setvar x
6 4 5 cop class x
7 1 3 6 cmpt class x ω × ω x
8 0 7 wceq wff 𝑔 = x ω × ω x