Metamath Proof Explorer

Table of Contents - 1.2.15. True and false constants

1. Universal quantifier for use by df-tru
   1. wal
2. Equality predicate for use by df-tru
   1. cv
   2. wceq
3. The true constant
   1. wtru
   2. trujust
   3. df-tru
   4. tru
   5. dftru2
   6. trut
   7. mptru
   8. tbtru
   9. bitru
   10. trud
   11. truan
4. The false constant
   1. wfal
   2. df-fal
   3. fal
   4. nbfal
   5. bifal
   6. falim
   7. falimd
   8. dfnot
   9. inegd
   10. efald
   11. pm2.21fal