Definition df-goal 35347

Description: Define the Godel-set of universal 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-goal	⊢ ∀𝑔𝑁𝑈 = ⟨2o, ⟨𝑁, 𝑈⟩⟩

Detailed syntax breakdown of Definition df-goal

Step	Hyp	Ref	Expression
1		cU	. . 3 class 𝑈
2		cN	. . 3 class 𝑁
3	1, 2	cgol 35340	. 2 class ∀𝑔𝑁𝑈
4		c2o 8500	. . 3 class 2o
5	2, 1	cop 4632	. . 3 class ⟨𝑁, 𝑈⟩
6	4, 5	cop 4632	. 2 class ⟨2o, ⟨𝑁, 𝑈⟩⟩
7	3, 6	wceq 1540	1 wff ∀𝑔𝑁𝑈 = ⟨2o, ⟨𝑁, 𝑈⟩⟩

This definition is referenced by:  goaleq12d  35356  gonanegoal  35357  sat1el2xp  35384  fmlaomn0  35395  goaln0  35398  goalrlem  35401  goalr  35402  fmla0disjsuc  35403  fmlasucdisj  35404  satffunlem1lem1  35407  satffunlem2lem1  35409