Metamath Proof Explorer


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
|- A.g N U = <. 2o , <. N , U >. >.

Detailed syntax breakdown

Step Hyp Ref Expression
0 cN
 |-  N
1 cU
 |-  U
2 1 0 cgol
 |-  A.g N U
3 c2o
 |-  2o
4 0 1 cop
 |-  <. N , U >.
5 3 4 cop
 |-  <. 2o , <. N , U >. >.
6 2 5 wceq
 |-  A.g N U = <. 2o , <. N , U >. >.