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

Definition df-tru 1541
 Description: Definition of the truth value "true", or "verum", denoted by ⊤. 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 instance of id 22 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 1542, and other proofs should use tru 1542 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 1542 instead. (New usage is discouraged.)
Assertion
Ref Expression
df-tru (⊤ ↔ (∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥))

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