Metamath Proof Explorer

Theorem ssiun3

Description: Subset equivalence for an indexed union. (Contributed by Thierry Arnoux, 17-Oct-2016)

Ref Expression
Assertion ssiun3 ⊢ ∀ y ∈ C ∃ x ∈ A y ∈ B ↔ C ⊆ ⋃ x ∈ A B

Proof

Step Hyp Ref Expression
1 df-ss ⊢ C ⊆ ⋃ x ∈ A B ↔ ∀ y y ∈ C → y ∈ ⋃ x ∈ A B
2 df-ral ⊢ ∀ y ∈ C y ∈ ⋃ x ∈ A B ↔ ∀ y y ∈ C → y ∈ ⋃ x ∈ A B
3 eliun ⊢ y ∈ ⋃ x ∈ A B ↔ ∃ x ∈ A y ∈ B
4 3 ralbii ⊢ ∀ y ∈ C y ∈ ⋃ x ∈ A B ↔ ∀ y ∈ C ∃ x ∈ A y ∈ B
5 1 2 4 3bitr2ri ⊢ ∀ y ∈ C ∃ x ∈ A y ∈ B ↔ C ⊆ ⋃ x ∈ A B