# 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";