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∈Ax⊆B

Proof

Step Hyp Ref Expression
1 eluni ⊢y∈⋃A↔∃xy∈x∧x∈A
2 1 imbi1i ⊢y∈⋃A→y∈B↔∃xy∈x∧x∈A→y∈B
3 19.23v ⊢∀xy∈x∧x∈A→y∈B↔∃xy∈x∧x∈A→y∈B
4 2 3 bitr4i ⊢y∈⋃A→y∈B↔∀xy∈x∧x∈A→y∈B
5 4 albii ⊢∀yy∈⋃A→y∈B↔∀y∀xy∈x∧x∈A→y∈B
6 alcom ⊢∀y∀xy∈x∧x∈A→y∈B↔∀x∀yy∈x∧x∈A→y∈B
7 19.21v ⊢∀yx∈A→y∈x→y∈B↔x∈A→∀yy∈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 ⊢∀yy∈x∧x∈A→y∈B↔∀yx∈A→y∈x→y∈B
12 df-ss ⊢x⊆B↔∀yy∈x→y∈B
13 12 imbi2i ⊢x∈A→x⊆B↔x∈A→∀yy∈x→y∈B
14 7 11 13 3bitr4i ⊢∀yy∈x∧x∈A→y∈B↔x∈A→x⊆B
15 14 albii ⊢∀x∀yy∈x∧x∈A→y∈B↔∀xx∈A→x⊆B
16 6 15 bitri ⊢∀y∀xy∈x∧x∈A→y∈B↔∀xx∈A→x⊆B
17 5 16 bitri ⊢∀yy∈⋃A→y∈B↔∀xx∈A→x⊆B
18 df-ss ⊢⋃A⊆B↔∀yy∈⋃A→y∈B
19 df-ral ⊢∀x∈Ax⊆B↔∀xx∈A→x⊆B
20 17 18 19 3bitr4i ⊢⋃A⊆B↔∀x∈Ax⊆B