Metamath Proof Explorer

Table of Contents - 21.50.3. Double restricted existential uniqueness

1. Restricted quantification (extension)
   1. r19.32
   2. rexsb
   3. rexrsb
   4. 2rexsb
   5. 2rexrsb
   6. cbvral2
   7. cbvrex2
   8. ralndv1
   9. ralndv2
2. Restricted uniqueness and "at most one" quantification
   1. reuf1odnf
   2. reuf1od
   3. euoreqb
3. Analogs to Existential uniqueness (double quantification)
   1. 2reu3
   2. 2reu7
   3. 2reu8
4. Additional theorems for double restricted existential uniqueness
   1. 2reu8i
   2. 2reuimp0
   3. 2reuimp