Definition df-goex 31341

Description: Define the Godel-set of existential quantification. Here N e. om corresponds to v_N , and U represents another formula, and this expression is [ E. x ph ] = E.g N U where x is the N-th variable, U = [ ph ] is the code for ph. Note that this is a class expression, not a wff. (Contributed by Mario Carneiro, 14-Jul-2013.)

Assertion

Ref	Expression
df-goex	|- E.g N U = -.g A.g N -.g U

Detailed syntax breakdown of Definition df-goex

Step	Hyp	Ref	Expression
1		cU	. . 3 class U
2		cN	. . 3 class N
3	1, 2	cgox 31334	. 2 class E.g N U
4	1	cgon 31328	. . . 4 class -.g U
5	4, 2	cgol 31317	. . 3 class A.g N -.g U
6	5	cgon 31328	. 2 class -.g A.g N -.g U
7	3, 6	wceq 1483	1 wff E.g N U = -.g A.g N -.g U

This definition is referenced by: (None)