Database
CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY
Predicate calculus with equality: Tarski's system S2 (1 rule, 6 schemes)
Rule scheme ax-gen (Generalization)
nfth
Metamath Proof Explorer
Description: No variable is (effectively) free in a theorem. (Contributed by Mario
Carneiro , 11-Aug-2016) df-nf changed. (Revised by Wolf Lammen , 12-Sep-2021)

Ref
Expression
Hypothesis
nfth.1
$${\u22a2}{\phi}$$
Assertion
nfth
$${\u22a2}\u2132{x}\phantom{\rule{.4em}{0ex}}{\phi}$$

Proof
Step
Hyp
Ref
Expression
1
nfth.1
$${\u22a2}{\phi}$$
2
nftht
$${\u22a2}\forall {x}\phantom{\rule{.4em}{0ex}}{\phi}\to \u2132{x}\phantom{\rule{.4em}{0ex}}{\phi}$$
3
2 1
mpg
$${\u22a2}\u2132{x}\phantom{\rule{.4em}{0ex}}{\phi}$$