This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iunssf

Description: Subset theorem for an indexed union. (Contributed by Glauco Siliprandi, 3-Mar-2021) Avoid ax-10 . (Revised by SN, 2-Feb-2026)

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-ss ⊢ ⋃ x ∈ A B ⊆ C ↔ ∀ y y ∈ ⋃ x ∈ A B → y ∈ C
3 eliun ⊢ y ∈ ⋃ x ∈ A B ↔ ∃ x ∈ A y ∈ B
4 3 imbi1i ⊢ y ∈ ⋃ x ∈ A B → y ∈ C ↔ ∃ x ∈ A y ∈ B → y ∈ C
5 4 albii ⊢ ∀ y y ∈ ⋃ x ∈ A B → y ∈ C ↔ ∀ y ∃ x ∈ A y ∈ B → y ∈ C
6 df-ss ⊢ B ⊆ C ↔ ∀ y y ∈ B → y ∈ C
7 6 ralbii ⊢ ∀ x ∈ A B ⊆ C ↔ ∀ x ∈ A ∀ y y ∈ B → y ∈ C
8 ralcom4 ⊢ ∀ x ∈ A ∀ y y ∈ B → y ∈ C ↔ ∀ y ∀ x ∈ A y ∈ B → y ∈ C
9 1 nfcri ⊢ Ⅎ x y ∈ C
10 9 r19.23 ⊢ ∀ x ∈ A y ∈ B → y ∈ C ↔ ∃ x ∈ A y ∈ B → y ∈ C
11 10 albii ⊢ ∀ y ∀ x ∈ A y ∈ B → y ∈ C ↔ ∀ y ∃ x ∈ A y ∈ B → y ∈ C
12 7 8 11 3bitrri ⊢ ∀ y ∃ x ∈ A y ∈ B → y ∈ C ↔ ∀ x ∈ A B ⊆ C
13 2 5 12 3bitri ⊢ ⋃ x ∈ A B ⊆ C ↔ ∀ x ∈ A B ⊆ C