no goals
x y : ZFSet
x✝¹ x✝ : PSet
α : Type u
A : α → PSet
β : Type u
B : β → PSet
⊢ PSet.mk β B ∈ PSet.powerset (PSet.mk α A) ↔ Quotient.mk setoid (PSet.mk β B) ⊆ Quotient.mk setoid (PSet.mk α A)
simp [mem_powerset, subset_iff]