# HG changeset patch
# User lcp
# Date 788197870 -3600
# Node ID 1aa6b351ca349e7b650a01d1cb901d1c6b5fdd40
# Parent  120edb26ee9322effcc54fc23b1fa59c1008f357
RepFun_eq_0_iff, RepFun_0: new

diff -r 120edb26ee93 -r 1aa6b351ca34 src/ZF/equalities.ML
--- 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";