Metamath Proof Explorer

Theorem iunss

Description: Subset theorem for an indexed union. (Contributed by NM, 13-Sep-2003) (Proof shortened by Andrew Salmon, 25-Jul-2011)

Ref Expression
Assertion iunss ⊢ ⋃ x ∈ A B ⊆ C ↔ ∀ x ∈ A B ⊆ C

Proof

Step Hyp Ref Expression
1 df-iun ⊢ ⋃ x ∈ A B = y | ∃ x ∈ A y ∈ B
2 1 sseq1i ⊢ ⋃ x ∈ A B ⊆ C ↔ y | ∃ x ∈ A y ∈ B ⊆ C
3 abss ⊢ y | ∃ x ∈ A y ∈ B ⊆ C ↔ ∀ y ∃ x ∈ A y ∈ B → y ∈ C
4 dfss2 ⊢ B ⊆ C ↔ ∀ y y ∈ B → y ∈ C
5 4 ralbii ⊢ ∀ x ∈ A B ⊆ C ↔ ∀ x ∈ A ∀ y y ∈ B → y ∈ C
6 ralcom4 ⊢ ∀ x ∈ A ∀ y y ∈ B → y ∈ C ↔ ∀ y ∀ x ∈ A y ∈ B → y ∈ C
7 r19.23v ⊢ ∀ x ∈ A y ∈ B → y ∈ C ↔ ∃ x ∈ A y ∈ B → y ∈ C
8 7 albii ⊢ ∀ y ∀ x ∈ A y ∈ B → y ∈ C ↔ ∀ y ∃ x ∈ A y ∈ B → y ∈ C
9 5 6 8 3bitrri ⊢ ∀ y ∃ x ∈ A y ∈ B → y ∈ C ↔ ∀ x ∈ A B ⊆ C
10 2 3 9 3bitri ⊢ ⋃ x ∈ A B ⊆ C ↔ ∀ x ∈ A B ⊆ C