Metamath Proof Explorer

Theorem iunssf

Description: Subset theorem for an indexed union. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypothesis iunssf.1 ⊢ Ⅎ _ x C
Assertion iunssf ⊢ ⋃ x ∈ A B ⊆ C ↔ ∀ x ∈ A B ⊆ C

Proof

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