Definition df-goex 35450

Description: Define the Godel-set of existential quantification. Here 𝑁 ∈ ω corresponds to v_N , and 𝑈 represents another formula, and this expression is [∃𝑥𝜑] = ∃_𝑔𝑁𝑈 where 𝑥 is the 𝑁-th variable, 𝑈 = [𝜑] is the code for 𝜑. Note that this is a class expression, not a wff. (Contributed by Mario Carneiro, 14-Jul-2013.)

Assertion

Ref	Expression
df-goex	⊢ ∃𝑔𝑁𝑈 = ¬𝑔∀𝑔𝑁¬𝑔𝑈

Detailed syntax breakdown of Definition df-goex

Step	Hyp	Ref	Expression
1		cU	. . 3 class 𝑈
2		cN	. . 3 class 𝑁
3	1, 2	cgox 35443	. 2 class ∃𝑔𝑁𝑈
4	1	cgon 35437	. . . 4 class ¬𝑔𝑈
5	4, 2	cgol 35340	. . 3 class ∀𝑔𝑁¬𝑔𝑈
6	5	cgon 35437	. 2 class ¬𝑔∀𝑔𝑁¬𝑔𝑈
7	3, 6	wceq 1540	1 wff ∃𝑔𝑁𝑈 = ¬𝑔∀𝑔𝑁¬𝑔𝑈

This definition is referenced by: (None)