Metamath Proof Explorer

Theorem unissb

Description: Relationship involving membership, subset, and union. Exercise 5 of Enderton p. 26 and its converse. (Contributed by NM, 20-Sep-2003) Avoid ax-11 . (Revised by BTernaryTau, 28-Dec-2024)

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

Proof

Step Hyp Ref Expression
1 eluni ⊢ y ∈ ⋃ A ↔ ∃ x y ∈ x ∧ x ∈ A
2 1 imbi1i ⊢ y ∈ ⋃ A → y ∈ B ↔ ∃ x y ∈ x ∧ x ∈ A → y ∈ B
3 19.23v ⊢ ∀ x y ∈ x ∧ x ∈ A → y ∈ B ↔ ∃ x y ∈ x ∧ x ∈ A → y ∈ B
4 2 3 bitr4i ⊢ y ∈ ⋃ A → y ∈ B ↔ ∀ x y ∈ x ∧ x ∈ A → y ∈ B
5 4 albii ⊢ ∀ y y ∈ ⋃ A → y ∈ B ↔ ∀ y ∀ x y ∈ x ∧ x ∈ A → y ∈ B
6 elequ1 ⊢ y = z → y ∈ x ↔ z ∈ x
7 6 anbi1d ⊢ y = z → y ∈ x ∧ x ∈ A ↔ z ∈ x ∧ x ∈ A
8 eleq1w ⊢ y = z → y ∈ B ↔ z ∈ B
9 7 8 imbi12d ⊢ y = z → y ∈ x ∧ x ∈ A → y ∈ B ↔ z ∈ x ∧ x ∈ A → z ∈ B
10 elequ2 ⊢ x = z → y ∈ x ↔ y ∈ z
11 eleq1w ⊢ x = z → x ∈ A ↔ z ∈ A
12 10 11 anbi12d ⊢ x = z → y ∈ x ∧ x ∈ A ↔ y ∈ z ∧ z ∈ A
13 12 imbi1d ⊢ x = z → y ∈ x ∧ x ∈ A → y ∈ B ↔ y ∈ z ∧ z ∈ A → y ∈ B
14 9 13 alcomw ⊢ ∀ y ∀ x y ∈ x ∧ x ∈ A → y ∈ B ↔ ∀ x ∀ y y ∈ x ∧ x ∈ A → y ∈ B
15 19.21v ⊢ ∀ y x ∈ A → y ∈ x → y ∈ B ↔ x ∈ A → ∀ y y ∈ x → y ∈ B
16 impexp ⊢ y ∈ x ∧ x ∈ A → y ∈ B ↔ y ∈ x → x ∈ A → y ∈ B
17 bi2.04 ⊢ y ∈ x → x ∈ A → y ∈ B ↔ x ∈ A → y ∈ x → y ∈ B
18 16 17 bitri ⊢ y ∈ x ∧ x ∈ A → y ∈ B ↔ x ∈ A → y ∈ x → y ∈ B
19 18 albii ⊢ ∀ y y ∈ x ∧ x ∈ A → y ∈ B ↔ ∀ y x ∈ A → y ∈ x → y ∈ B
20 df-ss ⊢ x ⊆ B ↔ ∀ y y ∈ x → y ∈ B
21 20 imbi2i ⊢ x ∈ A → x ⊆ B ↔ x ∈ A → ∀ y y ∈ x → y ∈ B
22 15 19 21 3bitr4i ⊢ ∀ y y ∈ x ∧ x ∈ A → y ∈ B ↔ x ∈ A → x ⊆ B
23 22 albii ⊢ ∀ x ∀ y y ∈ x ∧ x ∈ A → y ∈ B ↔ ∀ x x ∈ A → x ⊆ B
24 14 23 bitri ⊢ ∀ y ∀ x y ∈ x ∧ x ∈ A → y ∈ B ↔ ∀ x x ∈ A → x ⊆ B
25 5 24 bitri ⊢ ∀ y y ∈ ⋃ A → y ∈ B ↔ ∀ x x ∈ A → x ⊆ B
26 df-ss ⊢ ⋃ A ⊆ B ↔ ∀ y y ∈ ⋃ A → y ∈ B
27 df-ral ⊢ ∀ x ∈ A x ⊆ B ↔ ∀ x x ∈ A → x ⊆ B
28 25 26 27 3bitr4i ⊢ ⋃ A ⊆ B ↔ ∀ x ∈ A x ⊆ B