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

Definition df-gonot 33114
Description: Define the Godel-set of negation. Here the argument 𝑈 is also a Godel-set corresponding to smaller formulas. Note that this is a class expression, not a wff. (Contributed by Mario Carneiro, 14-Jul-2013.)
Assertion
Ref Expression
df-gonot ¬𝑔𝑈 = (𝑈𝑔𝑈)

Detailed syntax breakdown of Definition df-gonot
StepHypRef Expression
1 cU . . 3 class 𝑈
21cgon 33107 . 2 class ¬𝑔𝑈
3 cgna 33009 . . 3 class 𝑔
41, 1, 3co 7213 . 2 class (𝑈𝑔𝑈)
52, 4wceq 1543 1 wff ¬𝑔𝑈 = (𝑈𝑔𝑈)
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator