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
Next ⟩
wex
Metamath Proof Explorer
Ascii
Unicode
Table of Contents - 1.4.1.1. Existential quantifier
wex
df-ex
alnex
eximal