Add ssrexf to iset.mm

Copied without change from set.mm.

Fix capitalization in comment in set.mm and iset.mm.

Author: jkingdon

iset.mm

@@ -27458,6 +27458,16 @@ practical reasons (to avoid having to prove sethood of ` A ` in every use
   nelss $p |- ( ( A e. B /\ -. A e. C ) -> -. B C_ C ) $=
     ( wcel wss ssel com12 con3dimp ) ABDZBCEZACDZJIKBCAFGH $.
 
+  ${
+    ssrexf.1 $e |- F/_ x A $.
+    ssrexf.2 $e |- F/_ x B $.
+    $( Restricted existential quantification follows from a subclass
+       relationship.  (Contributed by Glauco Siliprandi, 20-Apr-2017.) $)
+    ssrexf $p |- ( A C_ B -> ( E. x e. A ph -> E. x e. B ph ) ) $=
+      ( wss cv wcel wa wex wrex nfss ssel anim1d eximd df-rex 3imtr4g ) CDGZBHZ
+      CIZAJZBKTDIZAJZBKABCLABDLSUBUDBBCDEFMSUAUCACDTNOPABCQABDQR $.
+  $}
+
   ${
     $d x A $.  $d x B $.
     $( Quantification restricted to a subclass.  (Contributed by NM,

set.mm

@@ -36527,7 +36527,7 @@ technically classes despite morally (and provably) being sets, like ` 1 `
   ${
     ssrexf.1 $e |- F/_ x A $.
     ssrexf.2 $e |- F/_ x B $.
-    $( restricted existential quantification follows from a subclass
+    $( Restricted existential quantification follows from a subclass
        relationship.  (Contributed by Glauco Siliprandi, 20-Apr-2017.) $)
     ssrexf $p |- ( A C_ B -> ( E. x e. A ph -> E. x e. B ph ) ) $=
       ( wss cv wcel wa wex wrex nfss ssel anim1d eximd df-rex 3imtr4g ) CDGZBHZ