Metamath Proof Explorer

Theorem ralssiun

Description: The index set of an indexed union is a subset of the union when each B contains its index. (Contributed by ML, 16-Dec-2020)

Ref Expression
Assertion ralssiun ⊢∀x∈Ax∈B→A⊆⋃x∈AB

Proof

Step Hyp Ref Expression
1 nfra1 ⊢Ⅎx∀x∈Ax∈B
2 nfcv ⊢Ⅎ_xA
3 nfiu1 ⊢Ⅎ_x⋃x∈AB
4 simpr ⊢x=y∧∀x∈Ax∈B∧x∈A→x∈A
5 rsp ⊢∀x∈Ax∈B→x∈A→x∈B
6 5 adantl ⊢x=y∧∀x∈Ax∈B→x∈A→x∈B
7 eleq1 ⊢x=y→x∈B↔y∈B
8 7 imbi2d ⊢x=y→x∈A→x∈B↔x∈A→y∈B
9 8 adantr ⊢x=y∧∀x∈Ax∈B→x∈A→x∈B↔x∈A→y∈B
10 6 9 mpbid ⊢x=y∧∀x∈Ax∈B→x∈A→y∈B
11 10 imp ⊢x=y∧∀x∈Ax∈B∧x∈A→y∈B
12 rspe ⊢x∈A∧y∈B→∃x∈Ay∈B
13 4 11 12 syl2anc ⊢x=y∧∀x∈Ax∈B∧x∈A→∃x∈Ay∈B
14 abid ⊢y∈y|∃x∈Ay∈B↔∃x∈Ay∈B
15 13 14 sylibr ⊢x=y∧∀x∈Ax∈B∧x∈A→y∈y|∃x∈Ay∈B
16 eleq1 ⊢x=y→x∈y|∃x∈Ay∈B↔y∈y|∃x∈Ay∈B
17 16 ad2antrr ⊢x=y∧∀x∈Ax∈B∧x∈A→x∈y|∃x∈Ay∈B↔y∈y|∃x∈Ay∈B
18 15 17 mpbird ⊢x=y∧∀x∈Ax∈B∧x∈A→x∈y|∃x∈Ay∈B
19 df-iun ⊢⋃x∈AB=y|∃x∈Ay∈B
20 18 19 eleqtrrdi ⊢x=y∧∀x∈Ax∈B∧x∈A→x∈⋃x∈AB
21 20 expl ⊢x=y→∀x∈Ax∈B∧x∈A→x∈⋃x∈AB
22 21 equcoms ⊢y=x→∀x∈Ax∈B∧x∈A→x∈⋃x∈AB
23 22 vtocleg ⊢x∈A→∀x∈Ax∈B∧x∈A→x∈⋃x∈AB
24 23 anabsi7 ⊢∀x∈Ax∈B∧x∈A→x∈⋃x∈AB
25 24 ex ⊢∀x∈Ax∈B→x∈A→x∈⋃x∈AB
26 1 2 3 25 ssrd ⊢∀x∈Ax∈B→A⊆⋃x∈AB