src/ZF/equalities.ML
changeset 787 1affbb1c5f1f
parent 760 f0200e91b272
child 839 1aa6b351ca34
--- a/src/ZF/equalities.ML	Wed Dec 14 16:54:13 1994 +0100
+++ b/src/ZF/equalities.ML	Wed Dec 14 16:57:55 1994 +0100
@@ -115,6 +115,10 @@
 by (fast_tac eq_cs 1);
 qed "Diff_0";
 
+goal ZF.thy "A-B=0 <-> A<=B";
+by (fast_tac (eq_cs addEs [equalityE]) 1);
+qed "Diff_eq_0_iff";
+
 (*NOT SUITABLE FOR REWRITING since {a} == cons(a,0)*)
 goal ZF.thy "A - cons(a,B) = A - B - {a}";
 by (fast_tac eq_cs 1);
@@ -450,6 +454,11 @@
 by (fast_tac eq_cs 1);
 qed "converse_diff";
 
+(*Does the analogue hold for INT?*)
+goal ZF.thy "converse(UN x:A. B(x)) = (UN x:A. converse(B(x)))";
+by (fast_tac eq_cs 1);
+qed "converse_UN";
+
 (** Pow **)
 
 goal ZF.thy "Pow(A) Un Pow(B) <= Pow(A Un B)";