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∈AB⊆C↔∀x∈AB⊆C

Proof

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