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 ∈ A x ∈ B → A ⊆ ⋃ x ∈ A B

Proof

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