Database
CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY
Predicate calculus with equality: Tarski's system S2 (1 rule, 6 schemes)
Rule scheme ax-gen (Generalization)
altru
Next ⟩
alfal
Metamath Proof Explorer
Ascii
Structured
Theorem
altru
Description:
For all sets,
T.
is true.
(Contributed by
Anthony Hart
, 13-Sep-2011)
Ref
Expression
Assertion
altru
⊢
∀
𝑥
⊤
Proof
Step
Hyp
Ref
Expression
1
tru
⊢
⊤
2
1
ax-gen
⊢
∀
𝑥
⊤