diff --git a/analysis/Analysis/Section_3_4.lean b/analysis/Analysis/Section_3_4.lean
index 1a5189196..26eca6677 100644
--- a/analysis/Analysis/Section_3_4.lean
+++ b/analysis/Analysis/Section_3_4.lean
@@ -391,6 +391,12 @@ theorem SetTheory.Set.image_preimage_of_surj {X Y:Set} (f:X → Y) :
 theorem SetTheory.Set.preimage_image_of_inj {X Y:Set} (f:X → Y) :
     (∀ S, S ⊆ X → preimage f (image f S) = S) ↔ Function.Injective f := by sorry
 
+/-- Helper lemma for Exercise 3.4.7. -/
+@[simp]
+lemma SetTheory.Set.mem_powerset' {S S' : Set} : (S': Object) ∈ S.powerset ↔ S' ⊆ S := by
+  rw [mem_powerset]
+  simp
+
 /-- Exercise 3.4.7 -/
 theorem SetTheory.Set.partial_functions {X Y:Set} :
     ∃ Z:Set, ∀ F:Object, F ∈ Z ↔ ∃ X' Y':Set, X' ⊆ X ∧ Y' ⊆ Y ∧ ∃ f: X' → Y', F = f := by