diff -r 42fb56041c11 -r 00ffae972fc0 src/HOL/Equiv_Relations.thy
--- a/src/HOL/Equiv_Relations.thy	Mon Oct 25 23:10:06 2021 +0200
+++ b/src/HOL/Equiv_Relations.thy	Tue Oct 26 11:15:40 2021 +0100
@@ -82,6 +82,9 @@
 lemma eq_equiv_class_iff: "equiv A r \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> r``{x} = r``{y} \<longleftrightarrow> (x, y) \<in> r"
   by (blast intro!: equiv_class_eq dest: eq_equiv_class equiv_type)
 
+lemma disjnt_equiv_class: "equiv A r \<Longrightarrow> disjnt (r``{a}) (r``{b}) \<longleftrightarrow> (a, b) \<notin> r"
+  by (auto dest: equiv_class_self simp: equiv_class_eq_iff disjnt_def)
+
 
 subsection \<open>Quotients\<close>