# HG changeset patch
# User desharna
# Date 1671096355 -3600
# Node ID 6b75499e52d1c0a5a8bf6e72fa5e216dd8abd8b9
# Parent  e772c8e6edd07e3ac4976a2977e720b71662c7c7
added antisymp_on_antisym_on_eq[pred_set_conv]

diff -r e772c8e6edd0 -r 6b75499e52d1 NEWS
--- a/NEWS	Thu Dec 15 10:24:21 2022 +0100
+++ b/NEWS	Thu Dec 15 10:25:55 2022 +0100
@@ -42,6 +42,7 @@
   - Added lemmas.
       antisym_if_asymp
       antisymp_if_asymp
+      antisymp_on_antisym_on_eq[pred_set_conv]
       asym_if_irrefl_and_trans
       asymp_if_irreflp_and_transp
       irreflD
diff -r e772c8e6edd0 -r 6b75499e52d1 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Thu Dec 15 10:24:21 2022 +0100
+++ b/src/HOL/Relation.thy	Thu Dec 15 10:25:55 2022 +0100
@@ -443,8 +443,11 @@
 
 text \<open>@{thm [source] antisym_def} and @{thm [source] antisymp_def} are for backward compatibility.\<close>
 
-lemma antisymp_antisym_eq [pred_set_conv]: "antisymp (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> antisym r"
-  by (simp add: antisym_def antisymp_def)
+lemma antisymp_on_antisym_on_eq[pred_set_conv]:
+  "antisymp_on A (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> antisym_on A r"
+  by (simp add: antisym_on_def antisymp_on_def)
+
+lemmas antisymp_antisym_eq = antisymp_on_antisym_on_eq[of UNIV]
 
 lemma antisymI [intro?]:
   "(\<And>x y. (x, y) \<in> r \<Longrightarrow> (y, x) \<in> r \<Longrightarrow> x = y) \<Longrightarrow> antisym r"