Metamath Proof Explorer


Table of Contents - 20.43.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. 2ralbiim
    9. ralndv1
    10. 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