Metamath Proof Explorer

Theorem unissbOLD

Description: Obsolete version of unissb as of 28-Dec-2024. (Contributed by NM, 20-Sep-2003) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion unissbOLD ⊢ ⋃ 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 df-ss ⊢ 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 df-ss ⊢ ⋃ 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