Add iunxprg to iset.mm

Copied without change from set.mm

Author: jkingdon

iset.mm

@@ -33562,6 +33562,20 @@ same disjoint variable group (meaning ` A ` cannot depend on ` x ` ) and
       RUIUEABCKUGUJUHUKAUDBDLAUDCDLMNAUDSDLUDUAUBOPQ $.
   $}
 
+  ${
+    $d x A $.  $d x B $.  $d x D $.  $d x E $.
+    iunxprg.1 $e |- ( x = A -> C = D ) $.
+    iunxprg.2 $e |- ( x = B -> C = E ) $.
+    $( A pair index picks out two instances of an indexed union's argument.
+       (Contributed by Alexander van der Vekens, 2-Feb-2018.) $)
+    iunxprg $p |- ( ( A e. V /\ B e. W )
+                    -> U_ x e. { A , B } C = ( D u. E ) ) $=
+      ( wcel wa cpr ciun csn cun wceq df-pr iuneq1 iunxsng iunxun adantr adantl
+      ax-mp eqtri uneq12d syl5eq ) BGKZCHKZLZABCMZDNZABOZDNZACOZDNZPZEFPULAUMUO
+      PZDNZUQUKURQULUSQBCRAUKURDSUDAUMUODUAUEUJUNEUPFUHUNEQUIABDEGITUBUIUPFQUHA
+      CDFHJTUCUFUG $.
+  $}
+
   ${
     $d x y z $.  $d x z A $.  $d z B $.  $d y z C $.
     $( Separate an indexed union in the index of an indexed union.