Database
CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY
Predicate calculus with equality: Tarski's system S2 (1 rule, 6 schemes)
Rule scheme ax-gen (Generalization)
alfal
Next ⟩
Axiom scheme ax-4 (Quantified Implication)
Metamath Proof Explorer
Ascii
Unicode
Theorem
alfal
Description:
For all sets,
-. F.
is true.
(Contributed by
Anthony Hart
, 13-Sep-2011)
Ref
Expression
Assertion
alfal
⊢
∀
x
¬
⊥
Proof
Step
Hyp
Ref
Expression
1
fal
⊢
¬
⊥
2
1
ax-gen
⊢
∀
x
¬
⊥