Definition df-tru

Description: Definition of the truth value "true", or "verum", denoted by T. . In this definition, an instance of id is used as the definiens, although any tautology, such as an axiom, can be used in its place. This particular instance of id 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 , and other proofs should use tru instead of this definition, since there are many alternate ways to define T. . (Contributed by Anthony Hart, 13-Oct-2010) (Revised by NM, 11-Jul-2019) Use tru instead. (New usage is discouraged.)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		wtru	⊢ ⊤
1		vx	⊢ 𝑥
2	1	cv	⊢ 𝑥
3	2 2	wceq	⊢ 𝑥 = 𝑥
4	3 1	wal	⊢ ∀ 𝑥 𝑥 = 𝑥
5	4 4	wi	⊢ ( ∀ 𝑥 𝑥 = 𝑥 → ∀ 𝑥 𝑥 = 𝑥 )
6	0 5	wb	⊢ ( ⊤ ↔ ( ∀ 𝑥 𝑥 = 𝑥 → ∀ 𝑥 𝑥 = 𝑥 ) )