# HG changeset patch
# User lcp
# Date 787420675 -3600
# Node ID 1affbb1c5f1f60f5cae18408985b49808b742155
# Parent  2a871417e7fc4f623828f38b56fc1d08f504fed2
converse_UN, Diff_eq_0_iff: new

diff -r 2a871417e7fc -r 1affbb1c5f1f src/ZF/equalities.ML
--- 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)";