Definition df-goal 31324

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

Assertion

Ref	Expression
df-goal	|- A.g N U = <. 2o , <. N , U >. >.

Detailed syntax breakdown of Definition df-goal

Step	Hyp	Ref	Expression
1		cU	. . 3 class U
2		cN	. . 3 class N
3	1, 2	cgol 31317	. 2 class A.g N U
4		c2o 7554	. . 3 class 2o
5	2, 1	cop 4183	. . 3 class <. N , U >.
6	4, 5	cop 4183	. 2 class <. 2o , <. N , U >. >.
7	3, 6	wceq 1483	1 wff A.g N U = <. 2o , <. N , U >. >.

This definition is referenced by: (None)