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"
Non-freeness predicate
Next ⟩
wnf
Metamath Proof Explorer
Ascii
Unicode
Table of Contents - 1.4.1.2. Non-freeness predicate
wnf
df-nf
nf2
nf3
nf4
nfi
nfri
nfd
nfrd
nftht
nfntht
nfntht2