LLPE Home Linear Logic Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  LLPE Home  >  Th. List  >  df-ex Structured version  

Definition df-ex 334
Description: Definition of existential quantifier. Dual of .
Assertion
Ref Expression
df-ex (∃x𝜑 ⧟ ~ ∀x~ 𝜑)

Detailed syntax breakdown of Definition df-ex
StepHypRef Expression
1 wph . . 3 wff 𝜑
2 vx . . 3 var x
31, 2wex 319 . 2 wffx𝜑
41wneg 3 . . . 4 wff ~ 𝜑
54, 2wal 318 . . 3 wffx~ 𝜑
65wneg 3 . 2 wff ~ ∀x~ 𝜑
73, 6wlb 55 1 wff (∃x𝜑 ⧟ ~ ∀x~ 𝜑)
Colors of variables: wff var nilad
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator