Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > dftru  Unicode version 
Description: Definition of the truth value "true", or "verum", denoted by . This is a tautology, as proved by tru 1399. 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 1399, and other proofs should depend on tru 1399 (directly or indirectly) instead of this definition, since there are many alternative ways to define . (Contributed by Anthony Hart, 13Oct2010.) (Revised by NM, 11Jul2019.) (New usage is discouraged.) 
Ref  Expression 

dftru 
No typesetting for:  ( T. <> ( A. x x = x > A. x x = x )
) 
Step  Hyp  Ref  Expression 

1  wtru 1396  . 2  
2  vx.tru 
. . . . . 6
No typesetting for: setvar x  
3  2  cv 1394 
. . . . 5
No typesetting for: class x 
4  3, 3  wceq 1395 
. . . 4
No typesetting for: wff x = x 
5  4, 2  wal 1393 
. . 3
No typesetting for: wff A. x x = x 
6  5, 5  wi 4 
. 2
No typesetting for: wff ( A. x x = x > A. x x = x ) 
7  1, 6  wb 184 
1
No typesetting for: wff ( T. <> ( A. x x = x > A. x x = x )
) 
Colors of variables: wff setvar class 
This definition is referenced by: tru 1399 
Copyright terms: Public domain  W3C validator 