Definition df-goex

Description: Define the Godel-set of existential quantification. Here N e.om corresponds to vN , 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)

	Ref	Expression
Assertion	df-goex	$$⊢\left[{\exists }_{𝑔}NU\right]=\left[{\neg }_{𝑔}\left[{\forall }_{𝑔}N\left[{\neg }_{𝑔}U\right]\right]\right]$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cN	$$classN$$
1		cU	$$classU$$
2	1 0	cgox	$$class\left[{\exists }_{𝑔}NU\right]$$
3	1	cgon	$$class\left[{\neg }_{𝑔}U\right]$$
4	3 0	cgol	$$class\left[{\forall }_{𝑔}N\left[{\neg }_{𝑔}U\right]\right]$$
5	4	cgon	$$class\left[{\neg }_{𝑔}\left[{\forall }_{𝑔}N\left[{\neg }_{𝑔}U\right]\right]\right]$$
6	2 5	wceq	$$wff\left[{\exists }_{𝑔}NU\right]=\left[{\neg }_{𝑔}\left[{\forall }_{𝑔}N\left[{\neg }_{𝑔}U\right]\right]\right]$$