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"
Nonfreeness predicate
wnf
Next ⟩
df-nf
Metamath Proof Explorer
Unicode
Structured
Syntax definition
wnf
Description:
Extend wff definition to include the not-free predicate.
Ref
Expression
Assertion
wnf
wff F/ x ph