diff -r c15ee153dec1 -r 812ce526da33 src/HOL/Library/FuncSet.thy
--- a/src/HOL/Library/FuncSet.thy	Wed Mar 20 23:06:51 2019 +0100
+++ b/src/HOL/Library/FuncSet.thy	Thu Mar 21 14:18:22 2019 +0000
@@ -550,6 +550,11 @@
 lemma PiE_eq_singleton: "(\<Pi>\<^sub>E i\<in>I. S i) = {\<lambda>i\<in>I. f i} \<longleftrightarrow> (\<forall>i\<in>I. S i = {f i})"
   by (metis (mono_tags, lifting) PiE_eq PiE_singleton insert_not_empty restrict_apply' restrict_extensional)
 
+lemma PiE_over_singleton_iff: "(\<Pi>\<^sub>E x\<in>{a}. B x) = (\<Union>b \<in> B a. {\<lambda>x \<in> {a}. b})"
+  apply (auto simp: PiE_iff split: if_split_asm)
+  apply (metis (no_types, lifting) extensionalityI restrict_apply' restrict_extensional singletonD)
+  done
+
 lemma all_PiE_elements:
    "(\<forall>z \<in> PiE I S. \<forall>i \<in> I. P i (z i)) \<longleftrightarrow> PiE I S = {} \<or> (\<forall>i \<in> I. \<forall>x \<in> S i. P i x)" (is "?lhs = ?rhs")
 proof (cases "PiE I S = {}")