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

Definition df-goex 33120
Description: Define the Godel-set of existential 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-goex 𝑔𝑁𝑈 = ¬𝑔𝑔𝑁¬𝑔𝑈

Detailed syntax breakdown of Definition df-goex
StepHypRef Expression
1 cU . . 3 class 𝑈
2 cN . . 3 class 𝑁
31, 2cgox 33113 . 2 class 𝑔𝑁𝑈
41cgon 33107 . . . 4 class ¬𝑔𝑈
54, 2cgol 33010 . . 3 class 𝑔𝑁¬𝑔𝑈
65cgon 33107 . 2 class ¬𝑔𝑔𝑁¬𝑔𝑈
73, 6wceq 1543 1 wff 𝑔𝑁𝑈 = ¬𝑔𝑔𝑁¬𝑔𝑈
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator