added lemma symp_on_sym_on_eq[pred_set_conv]

--- a/NEWS	Fri Dec 16 10:13:52 2022 +0100
+++ b/NEWS	Fri Dec 16 10:18:35 2022 +0100
@@ -79,6 +79,7 @@
       preorder.reflp_on_ge[simp]
       preorder.reflp_on_le[simp]
       reflp_on_conversp[simp]
+      symp_on_sym_on_eq[pred_set_conv]
       totalI
       totalp_on_converse[simp]
       totalp_on_singleton[simp]

--- a/src/HOL/Relation.thy	Fri Dec 16 10:13:52 2022 +0100
+++ b/src/HOL/Relation.thy	Fri Dec 16 10:18:35 2022 +0100
@@ -381,8 +381,10 @@
 
 text \<open>@{thm [source] sym_def} and @{thm [source] symp_def} are for backward compatibility.\<close>
 
-lemma symp_sym_eq [pred_set_conv]: "symp (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> sym r"
-  by (simp add: sym_def symp_def)
+lemma symp_on_sym_on_eq[pred_set_conv]: "symp_on A (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> sym_on A r"
+  by (simp add: sym_on_def symp_on_def)
+
+lemmas symp_sym_eq = symp_on_sym_on_eq[of UNIV] \<comment> \<open>For backward compatibility\<close>
 
 lemma symI [intro?]: "(\<And>a b. (a, b) \<in> r \<Longrightarrow> (b, a) \<in> r) \<Longrightarrow> sym r"
   by (unfold sym_def) iprover