# HG changeset patch # User lcp # Date 756478692 -3600 # Node ID 0f0ff91b07f627df8ca9913de425b90affb60c4c # Parent 7c7179e687b21d2ba21a56d4eec6a96032cd0f34 new section for equality properties diff -r 7c7179e687b2 -r 0f0ff91b07f6 src/ZF/equalities.ML --- a/src/ZF/equalities.ML Tue Dec 14 14:02:52 1993 +0100 +++ b/src/ZF/equalities.ML Tue Dec 21 13:58:12 1993 +0100 @@ -322,3 +322,28 @@ by (fast_tac eq_cs 1); val converse_diff = result(); +(** Pow **) + +goal ZF.thy "Pow(A) Un Pow(B) <= Pow(A Un B)"; +by (fast_tac upair_cs 1); +val Un_Pow_subset = result(); + +goal ZF.thy "(UN x:A. Pow(B(x))) <= Pow(UN x:A. B(x))"; +by (fast_tac upair_cs 1); +val UN_Pow_subset = result(); + +goal ZF.thy "A <= Pow(Union(A))"; +by (fast_tac upair_cs 1); +val subset_Pow_Union = result(); + +goal ZF.thy "Union(Pow(A)) = A"; +by (fast_tac eq_cs 1); +val Union_Pow_eq = result(); + +goal ZF.thy "Pow(A) Int Pow(B) = Pow(A Int B)"; +by (fast_tac eq_cs 1); +val Int_Pow_eq = result(); + +goal ZF.thy "!!x A. x:A ==> (INT x:A. Pow(B(x))) = Pow(INT x:A. B(x))"; +by (fast_tac eq_cs 1); +val INT_Pow_subset = result();