Add dmmptd to iset.mm

Copied without change from set.mm.

Author: jkingdon

iset.mm

@@ -46497,6 +46497,17 @@ We use their notation ("onto" under the arrow).  (Contributed by NM,
       ( wfn cdm wceq fnmpti fndm ax-mp ) DBGDHBIABCDEFJBDKL $.
   $}
 
+  ${
+    $d B x $.  $d ph x $.
+    dmmptd.a $e |- A = ( x e. B |-> C ) $.
+    dmmptd.c $e |- ( ( ph /\ x e. B ) -> C e. V ) $.
+    $( The domain of the mapping operation, deduction form.  (Contributed by
+       Glauco Siliprandi, 11-Dec-2019.) $)
+    dmmptd $p |- ( ph -> dom A = B ) $=
+      ( cvv wcel crab cdm wral wceq cv wa elexd ralrimiva rabid2 sylibr dmmpt
+      syl6reqr ) ADEIJZBDKZCLAUCBDMDUDNAUCBDABODJPEFHQRUCBDSTBDECGUAUB $.
+  $}
+
   ${
     $d x y $.  $d y A $.  $d y B $.  $d y C $.
     $( Union of mappings which are mutually compatible.  (Contributed by Mario