case h
α : Type u_1
β : Type ?u.65383
γ : Type ?u.65386
ι : Sort u_2
ι' : Sort ?u.65392
ι₂ : Sort ?u.65395
κ : ι → Sort ?u.65400
κ₁ : ι → Sort ?u.65405
κ₂ : ι → Sort ?u.65410
κ' : ι' → Sort ?u.65415
P : ι → α → Prop
x✝ : α
⊢ (x✝ ∈ ⋂ (i : ι), {x | P i x}) ↔ x✝ ∈ {x | ∀ (i : ι), P i x}
α : Type u_1
β : Type ?u.65383
γ : Type ?u.65386
ι : Sort u_2
ι' : Sort ?u.65392
ι₂ : Sort ?u.65395
κ : ι → Sort ?u.65400
κ₁ : ι → Sort ?u.65405
κ₂ : ι → Sort ?u.65410
κ' : ι' → Sort ?u.65415
P : ι → α → Prop
⊢ (⋂ (i : ι), {x | P i x}) = {x | ∀ (i : ι), P i x}
ext
no goals
case h
α : Type u_1
β : Type ?u.65383
γ : Type ?u.65386
ι : Sort u_2
ι' : Sort ?u.65392
ι₂ : Sort ?u.65395
κ : ι → Sort ?u.65400
κ₁ : ι → Sort ?u.65405
κ₂ : ι → Sort ?u.65410
κ' : ι' → Sort ?u.65415
P : ι → α → Prop
x✝ : α
⊢ (x✝ ∈ ⋂ (i : ι), {x | P i x}) ↔ x✝ ∈ {x | ∀ (i : ι), P i x}
exact mem_iInter