Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-goal Structured version   Visualization version   GIF version

Definition df-goal 33324
Description: Define the Godel-set of universal quantification. Here 𝑁 ∈ ω corresponds to vN , 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
StepHypRef Expression
1 cU . . 3 class 𝑈
2 cN . . 3 class 𝑁
31, 2cgol 33317 . 2 class 𝑔𝑁𝑈
4 c2o 8303 . . 3 class 2o
52, 1cop 4571 . . 3 class 𝑁, 𝑈
64, 5cop 4571 . 2 class ⟨2o, ⟨𝑁, 𝑈⟩⟩
73, 6wceq 1538 1 wff 𝑔𝑁𝑈 = ⟨2o, ⟨𝑁, 𝑈⟩⟩
Colors of variables: wff setvar class
This definition is referenced by:  goaleq12d  33333  gonanegoal  33334  sat1el2xp  33361  fmlaomn0  33372  goaln0  33375  goalrlem  33378  goalr  33379  fmla0disjsuc  33380  fmlasucdisj  33381  satffunlem1lem1  33384  satffunlem2lem1  33386
  Copyright terms: Public domain W3C validator