Metamath Proof Explorer

Table of Contents - 21.3.2. Predicate Calculus

1. Predicate Calculus - misc additions
   1. sbc2iedf
   2. rspc2daf
2. Restricted quantification - misc additions
   1. ralcom4f
   2. rexcom4f
   3. 19.9d2rf
   4. 19.9d2r
   5. r19.29ffa
   6. n0limd
   7. reu6dv
3. Equality
   1. eqtrb
   2. eqelbid
4. Double restricted existential uniqueness quantification
   1. opsbc2ie
   2. opreu2reuALT
5. Double restricted existential uniqueness quantification syntax
   1. w2reu
   2. df-2reu
   3. 2reucom
   4. 2reu2rex1
   5. 2reureurex
   6. 2reu2reu2
   7. opreu2reu1
   8. sq2reunnltb
   9. addsqnot2reu
6. Substitution (without distinct variables) - misc additions
   1. sbceqbidf
   2. sbcies
7. Existential "at most one" - misc additions
   1. mo5f
   2. nmo
8. Existential uniqueness - misc additions
   1. reuxfrdf
   2. rexunirn
9. Restricted "at most one" - misc additions
   1. rmoxfrd
   2. rmoun
   3. rmounid
10. Restricted iota (description binder)
    1. riotaeqbidva