α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t✝ t₁ t₂ u : Set α
p : Prop
inst✝ : Decidable p
t : p → Set α
x : α
⊢ (∀ (h : p), x ∈ t h) ∧ p ↔ ∃ h, x ∈ t h
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t✝ t₁ t₂ u : Set α
p : Prop
inst✝ : Decidable p
t : p → Set α
x : α
⊢ (x ∈ if h : p then t h else ∅) ↔ ∃ h, x ∈ t h
simp only [mem_dite, mem_empty_iff_false, imp_false, not_not]
no goals
α : Type u
β : Type v
γ : Type w
ι : Sort x
a b : α
s s₁ s₂ t✝ t₁ t₂ u : Set α
p : Prop
inst✝ : Decidable p
t : p → Set α
x : α
⊢ (∀ (h : p), x ∈ t h) ∧ p ↔ ∃ h, x ∈ t h
exact ⟨fun h => ⟨h.2, h.1 h.2⟩, fun ⟨h₁, h₂⟩ => ⟨fun _ => h₂, h₁⟩⟩