Metamath Proof Explorer

Table of Contents - 1.4.1. Universal quantifier (continued); define "exists" and "not free"

The universal quantifier was introduced above in wal for use by df-tru. See the comments in that section. In this section, we continue with the first "real" use of it.

1. Existential quantifier
   1. wex
   2. df-ex
   3. alnex
   4. eximal
2. Non-freeness predicate
   1. wnf
   2. df-nf
   3. nf2
   4. nf3
   5. nf4
   6. nfi
   7. nfri
   8. nfd
   9. nfrd
   10. nftht
   11. nfntht
   12. nfntht2