Add funfnd to iset.mm

Copied without change from set.mm.

Author: jkingdon

iset.mm

@@ -45510,6 +45510,14 @@ We use their notation ("onto" under the arrow).  (Contributed by NM,
     ( wfun cdm wceq wa wfn eqid biantru df-fn bitr4i ) ABZKACZLDZEALFMKLGHALIJ
     $.
 
+  ${
+    funfnd.1 $e |- ( ph -> Fun A ) $.
+    $( A function is a function over its domain.  (Contributed by Glauco
+       Siliprandi, 23-Oct-2021.) $)
+    funfnd $p |- ( ph -> A Fn dom A ) $=
+      ( wfun cdm wfn funfn sylib ) ABDBBEFCBGH $.
+  $}
+
   $( The identity relation is a function.  Part of Theorem 10.4 of [Quine]
      p. 65.  (Contributed by NM, 30-Apr-1998.) $)
   funi $p |- Fun _I $=