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)

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 alcom ⊢ ∀ y ∀ x y ∈ x ∧ x ∈ A → y ∈ B ↔ ∀ x ∀ y y ∈ x ∧ x ∈ A → y ∈ B
7 19.21v ⊢ ∀ y x ∈ A → y ∈ x → y ∈ B ↔ x ∈ A → ∀ y y ∈ x → y ∈ B
8 impexp ⊢ y ∈ x ∧ x ∈ A → y ∈ B ↔ y ∈ x → x ∈ A → y ∈ B
9 bi2.04 ⊢ y ∈ x → x ∈ A → y ∈ B ↔ x ∈ A → y ∈ x → y ∈ B
10 8 9 bitri ⊢ y ∈ x ∧ x ∈ A → y ∈ B ↔ x ∈ A → y ∈ x → y ∈ B
11 10 albii ⊢ ∀ y y ∈ x ∧ x ∈ A → y ∈ B ↔ ∀ y x ∈ A → y ∈ x → y ∈ B
12 dfss2 ⊢ x ⊆ B ↔ ∀ y y ∈ x → y ∈ B
13 12 imbi2i ⊢ x ∈ A → x ⊆ B ↔ x ∈ A → ∀ y y ∈ x → y ∈ B
14 7 11 13 3bitr4i ⊢ ∀ y y ∈ x ∧ x ∈ A → y ∈ B ↔ x ∈ A → x ⊆ B
15 14 albii ⊢ ∀ x ∀ y y ∈ x ∧ x ∈ A → y ∈ B ↔ ∀ x x ∈ A → x ⊆ B
16 6 15 bitri ⊢ ∀ y ∀ x y ∈ x ∧ x ∈ A → y ∈ B ↔ ∀ x x ∈ A → x ⊆ B
17 5 16 bitri ⊢ ∀ y y ∈ ⋃ A → y ∈ B ↔ ∀ x x ∈ A → x ⊆ B
18 dfss2 ⊢ ⋃ A ⊆ B ↔ ∀ y y ∈ ⋃ A → y ∈ B
19 df-ral ⊢ ∀ x ∈ A x ⊆ B ↔ ∀ x x ∈ A → x ⊆ B
20 17 18 19 3bitr4i ⊢ ⋃ A ⊆ B ↔ ∀ x ∈ A x ⊆ B