Database
CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY
Predicate calculus with equality: Tarski's system S2 (1 rule, 6 schemes)
Rule scheme ax-gen (Generalization)
nffal
Next ⟩
sptruw
Metamath Proof Explorer
Ascii
Structured
Theorem
nffal
Description:
The false constant has no free variables (see
nftru
).
(Contributed by
BJ
, 6-May-2019)
Ref
Expression
Assertion
nffal
⊢
Ⅎ
𝑥
⊥
Proof
Step
Hyp
Ref
Expression
1
fal
⊢
¬ ⊥
2
1
nfnth
⊢
Ⅎ
𝑥
⊥