MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-tru Structured version   Visualization version   GIF version

Definition df-tru 1478
Description: Definition of the truth value "true", or "verum", denoted by . This is a tautology, as proved by tru 1479. In this definition, an instance of id 22 is used as the definiens, although any tautology, such as an axiom, can be used in its place. This particular id 22 instance 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 1479, and other proofs should depend on tru 1479 (directly or indirectly) instead of this definition, since there are many alternative ways to define . (Contributed by Anthony Hart, 13-Oct-2010.) (Revised by NM, 11-Jul-2019.) (New usage is discouraged.)
Assertion
Ref Expression
df-tru (⊤ ↔ (∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥))

Detailed syntax breakdown of Definition df-tru
StepHypRef Expression
1 wtru 1476 . 2 wff
2 vx.tru . . . . . 6 setvar 𝑥
32cv 1474 . . . . 5 class 𝑥
43, 3wceq 1475 . . . 4 wff 𝑥 = 𝑥
54, 2wal 1473 . . 3 wff 𝑥 𝑥 = 𝑥
65, 5wi 4 . 2 wff (∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥)
71, 6wb 195 1 wff (⊤ ↔ (∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥))
Colors of variables: wff setvar class
This definition is referenced by:  tru  1479
  Copyright terms: Public domain W3C validator