no goals
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
t : Set (PrimeSpectrum R)
f : R
⊢ f ∈ vanishingIdeal t ↔ ∀ (x : PrimeSpectrum R), x ∈ t → f ∈ x.asIdeal
rw [← SetLike.mem_coe, coe_vanishingIdeal, Set.mem_setOf_eq]