RepFun_eq_0_iff, RepFun_0: new

--- a/src/ZF/equalities.ML	Fri Dec 23 16:50:22 1994 +0100
+++ b/src/ZF/equalities.ML	Fri Dec 23 16:51:10 1994 +0100
@@ -485,3 +485,12 @@
 by (fast_tac eq_cs 1);
 qed "INT_Pow_subset";
 
+(** RepFun **)
+
+goal ZF.thy "{f(x).x:A}=0 <-> A=0";
+by (fast_tac (eq_cs addSEs [equalityE]) 1);
+qed "RepFun_eq_0_iff";
+
+goal ZF.thy "{f(x).x:0} = 0";
+by (fast_tac eq_cs 1);
+qed "RepFun_0";