case h
α : Type u_1
β : Type ?u.65233
γ : Type ?u.65236
ι : Sort u_2
ι' : Sort ?u.65242
ι₂ : Sort ?u.65245
κ : ι → Sort ?u.65250
κ₁ : ι → Sort ?u.65255
κ₂ : ι → Sort ?u.65260
κ' : ι' → Sort ?u.65265
P : ι → α → Prop
x✝ : α
⊢ (x✝ ∈ ⋃ (i : ι), {x | P i x}) ↔ x✝ ∈ {x | ∃ i, P i x}
α : Type u_1
β : Type ?u.65233
γ : Type ?u.65236
ι : Sort u_2
ι' : Sort ?u.65242
ι₂ : Sort ?u.65245
κ : ι → Sort ?u.65250
κ₁ : ι → Sort ?u.65255
κ₂ : ι → Sort ?u.65260
κ' : ι' → Sort ?u.65265
P : ι → α → Prop
⊢ (⋃ (i : ι), {x | P i x}) = {x | ∃ i, P i x}
ext
no goals
case h
α : Type u_1
β : Type ?u.65233
γ : Type ?u.65236
ι : Sort u_2
ι' : Sort ?u.65242
ι₂ : Sort ?u.65245
κ : ι → Sort ?u.65250
κ₁ : ι → Sort ?u.65255
κ₂ : ι → Sort ?u.65260
κ' : ι' → Sort ?u.65265
P : ι → α → Prop
x✝ : α
⊢ (x✝ ∈ ⋃ (i : ι), {x | P i x}) ↔ x✝ ∈ {x | ∃ i, P i x}
exact mem_iUnion