Definition df-goal

Description: Define the Godel-set of universal quantification. Here N e.om corresponds to vN , and U represents another formula, and this expression is [ A. x ph ] = A.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-goal	⊢ ∀𝑔 𝑁 𝑈 = ⟨ 2o , ⟨ 𝑁 , 𝑈 ⟩ ⟩

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cN	⊢ 𝑁
1		cU	⊢ 𝑈
2	1 0	cgol	⊢ ∀𝑔 𝑁 𝑈
3		c2o	⊢ 2o
4	0 1	cop	⊢ ⟨ 𝑁 , 𝑈 ⟩
5	3 4	cop	⊢ ⟨ 2o , ⟨ 𝑁 , 𝑈 ⟩ ⟩
6	2 5	wceq	⊢ ∀𝑔 𝑁 𝑈 = ⟨ 2o , ⟨ 𝑁 , 𝑈 ⟩ ⟩