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∈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 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∀xy∈x∧x∈A→y∈B↔∀x∀yy∈x∧x∈A→y∈B
15 19.21v ⊢∀yx∈A→y∈x→y∈B↔x∈A→∀yy∈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 ⊢∀yy∈x∧x∈A→y∈B↔∀yx∈A→y∈x→y∈B
20 dfss2 ⊢x⊆B↔∀yy∈x→y∈B
21 20 imbi2i ⊢x∈A→x⊆B↔x∈A→∀yy∈x→y∈B
22 15 19 21 3bitr4i ⊢∀yy∈x∧x∈A→y∈B↔x∈A→x⊆B
23 22 albii ⊢∀x∀yy∈x∧x∈A→y∈B↔∀xx∈A→x⊆B
24 14 23 bitri ⊢∀y∀xy∈x∧x∈A→y∈B↔∀xx∈A→x⊆B
25 5 24 bitri ⊢∀yy∈⋃A→y∈B↔∀xx∈A→x⊆B
26 dfss2 ⊢⋃A⊆B↔∀yy∈⋃A→y∈B
27 df-ral ⊢∀x∈Ax⊆B↔∀xx∈A→x⊆B
28 25 26 27 3bitr4i ⊢⋃A⊆B↔∀x∈Ax⊆B