Metamath Proof Explorer

Theorem iinuni

Description: A relationship involving union and indexed intersection. Exercise 23 of Enderton p. 33. (Contributed by NM, 25-Nov-2003) (Proof shortened by Mario Carneiro, 17-Nov-2016)

Ref Expression
Assertion iinuni ⊢ A ∪ ⋂ B = ⋂ x ∈ B A ∪ x

Proof

Step Hyp Ref Expression
1 r19.32v ⊢ ∀ x ∈ B y ∈ A ∨ y ∈ x ↔ y ∈ A ∨ ∀ x ∈ B y ∈ x
2 elun ⊢ y ∈ A ∪ x ↔ y ∈ A ∨ y ∈ x
3 2 ralbii ⊢ ∀ x ∈ B y ∈ A ∪ x ↔ ∀ x ∈ B y ∈ A ∨ y ∈ x
4 vex ⊢ y ∈ V
5 4 elint2 ⊢ y ∈ ⋂ B ↔ ∀ x ∈ B y ∈ x
6 5 orbi2i ⊢ y ∈ A ∨ y ∈ ⋂ B ↔ y ∈ A ∨ ∀ x ∈ B y ∈ x
7 1 3 6 3bitr4ri ⊢ y ∈ A ∨ y ∈ ⋂ B ↔ ∀ x ∈ B y ∈ A ∪ x
8 7 abbii ⊢ y | y ∈ A ∨ y ∈ ⋂ B = y | ∀ x ∈ B y ∈ A ∪ x
9 df-un ⊢ A ∪ ⋂ B = y | y ∈ A ∨ y ∈ ⋂ B
10 df-iin ⊢ ⋂ x ∈ B A ∪ x = y | ∀ x ∈ B y ∈ A ∪ x
11 8 9 10 3eqtr4i ⊢ A ∪ ⋂ B = ⋂ x ∈ B A ∪ x