Definition df-tru 1571

Description: Definition of the truth value "true", or "verum", denoted by ⊤. In this definition, an instance of id 23 is used as the definiens, although any tautology, such as an axiom, can be used in its place. This particular instance of id 23 was chosen so this definition can be checked by the same algorithm that is used for predicate calculus. This definition should be referenced directly only by tru 1572, and other proofs should use tru 1572 instead of this definition, since there are many alternate ways to define ⊤. (Contributed by Anthony Hart, 13-Oct-2010.) (Revised by NM, 11-Jul-2019.) Use tru 1572 instead. (New usage is discouraged.)

Assertion

Ref	Expression
df-tru	⊢ (⊤ ↔ (∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥))

Detailed syntax breakdown of Definition df-tru

Step	Hyp	Ref	Expression
1		wtru 1569	. 2 wff ⊤
2		vx.tru	. . . . . 6 setvar 𝑥
3	2	cv 1567	. . . . 5 class 𝑥
4	3, 3	wceq 1568	. . . 4 wff 𝑥 = 𝑥
5	4, 2	wal 1566	. . 3 wff ∀𝑥 𝑥 = 𝑥
6	5, 5	wi 4	. 2 wff (∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥)
7	1, 6	wb 209	1 wff (⊤ ↔ (∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥))

This definition is referenced by:  tru  1572