Add ssrmof to iset.mm

Copied without change from set.mm.

Author: jkingdon

iset.mm

@@ -27466,6 +27466,13 @@ practical reasons (to avoid having to prove sethood of ` A ` in every use
     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 $.
+
+    $( "At most one" existential quantification restricted to a subclass.
+       (Contributed by Thierry Arnoux, 8-Oct-2017.) $)
+    ssrmof $p |- ( A C_ B -> ( E* x e. B ph -> E* x e. A ph ) ) $=
+      ( wss cv wcel wa wmo wrmo wi wal dfss2f biimpi pm3.45 alimi moim df-rmo
+      3syl 3imtr4g ) CDGZBHZDIZAJZBKZUDCIZAJZBKZABDLABCLUCUHUEMZBNZUIUFMZBNUGUJ
+      MUCULBCDEFOPUKUMBUHUEAQRUIUFBSUAABDTABCTUB $.
   $}
 
   ${