| changeset 76214 | 0c18df79b1c8 |
| parent 76213 | e44d86131648 |
| child 76215 | a642599ffdea |
--- a/src/ZF/EquivClass.thy Tue Sep 27 16:51:35 2022 +0100 +++ b/src/ZF/EquivClass.thy Tue Sep 27 17:03:23 2022 +0100 @@ -92,7 +92,7 @@ by (unfold equiv_def, blast) lemma equiv_class_eq_iff: - "equiv(A,r) \<Longrightarrow> <x,y>: r \<longleftrightarrow> r``{x} = r``{y} & x \<in> A & y \<in> A" + "equiv(A,r) \<Longrightarrow> <x,y>: r \<longleftrightarrow> r``{x} = r``{y} \<and> x \<in> A \<and> y \<in> A" by (blast intro: eq_equiv_class equiv_class_eq dest: equiv_type) lemma eq_equiv_class_iff: