Database
CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY
Predicate calculus with equality: Tarski's system S2 (1 rule, 6 schemes)
Universal quantifier (continued); define "exists" and "not free"
Existential quantifier
wex
Next ⟩
df-ex
Metamath Proof Explorer
Ascii
Structured
Syntax definition
wex
Description:
Extend wff definition to include the existential quantifier ("there exists").
Ref
Expression
Assertion
wex
wff
∃
𝑥
𝜑