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

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) Avoid ax-10 , ax-12 . (Revised by SN, 2-Feb-2026)

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

Proof

Step Hyp Ref Expression
1 df-ss ⊢ ⋃ x ∈ A B ⊆ C ↔ ∀ y y ∈ ⋃ x ∈ A B → y ∈ C
2 eliun ⊢ y ∈ ⋃ x ∈ A B ↔ ∃ x ∈ A y ∈ B
3 2 imbi1i ⊢ y ∈ ⋃ x ∈ A B → y ∈ C ↔ ∃ x ∈ A y ∈ B → y ∈ C
4 3 albii ⊢ ∀ y y ∈ ⋃ x ∈ A B → y ∈ C ↔ ∀ y ∃ x ∈ A y ∈ B → y ∈ C
5 df-ss ⊢ 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 r19.23v ⊢ ∀ x ∈ A y ∈ B → y ∈ C ↔ ∃ x ∈ A y ∈ B → y ∈ C
9 8 albii ⊢ ∀ y ∀ x ∈ A y ∈ B → y ∈ C ↔ ∀ y ∃ x ∈ A y ∈ B → y ∈ C
10 6 7 9 3bitrri ⊢ ∀ y ∃ x ∈ A y ∈ B → y ∈ C ↔ ∀ x ∈ A B ⊆ C
11 1 4 10 3bitri ⊢ ⋃ x ∈ A B ⊆ C ↔ ∀ x ∈ A B ⊆ C