Description: Restricted quantifier version of exlimi . For a version based on fewer axioms see rexlimiv . (Contributed by NM, 30-Nov-2003) (Proof shortened by Andrew Salmon, 30-May-2011)