Definition df-goel 31322

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₀ e. v₁ , not 0 e. 1. (Contributed by Mario Carneiro, 14-Jul-2013.)

Assertion

Ref	Expression
df-goel	|- e.g = ( x e. ( om X. om ) |-> <. (/) , x >. )

Detailed syntax breakdown of Definition df-goel

Step	Hyp	Ref	Expression
1		cgoe 31315	. 2 class e.g
2		vx	. . 3 setvar x
3		com 7065	. . . 4 class om
4	3, 3	cxp 5112	. . 3 class ( om X. om )
5		c0 3915	. . . 4 class (/)
6	2	cv 1482	. . . 4 class x
7	5, 6	cop 4183	. . 3 class <. (/) , x >.
8	2, 4, 7	cmpt 4729	. 2 class ( x e. ( om X. om ) |-> <. (/) , x >. )
9	1, 8	wceq 1483	1 wff e.g = ( x e. ( om X. om ) |-> <. (/) , x >. )

This definition is referenced by: (None)