Metamath Proof Explorer

Theorem iunssf

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

Ref Expression
Hypothesis iunssf.1 ⊢Ⅎ_xC
Assertion iunssf ⊢⋃x∈AB⊆C↔∀x∈AB⊆C

Proof

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