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
nftht
Metamath Proof Explorer
Description: Closed form of nfth . (Contributed by Wolf Lammen , 19-Aug-2018)
(Proof shortened by BJ , 16-Sep-2021) (Proof shortened by Wolf Lammen , 3-Sep-2022)

Ref
Expression
Assertion
nftht
$${\u22a2}\forall {x}\phantom{\rule{.4em}{0ex}}{\phi}\to \u2132{x}\phantom{\rule{.4em}{0ex}}{\phi}$$

Proof
Step
Hyp
Ref
Expression
1
ax-1
$${\u22a2}\forall {x}\phantom{\rule{.4em}{0ex}}{\phi}\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi}\to \forall {x}\phantom{\rule{.4em}{0ex}}{\phi}\right)$$
2
1
nfd
$${\u22a2}\forall {x}\phantom{\rule{.4em}{0ex}}{\phi}\to \u2132{x}\phantom{\rule{.4em}{0ex}}{\phi}$$