![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > unissb | Structured version Visualization version GIF version |
Description: Relationship involving membership, subset, and union. Exercise 5 of [Enderton] p. 26 and its converse. (Contributed by NM, 20-Sep-2003.) |
Ref | Expression |
---|---|
unissb | ⊢ (∪ 𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eluni 4803 | . . . . . 6 ⊢ (𝑦 ∈ ∪ 𝐴 ↔ ∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴)) | |
2 | 1 | imbi1i 353 | . . . . 5 ⊢ ((𝑦 ∈ ∪ 𝐴 → 𝑦 ∈ 𝐵) ↔ (∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵)) |
3 | 19.23v 1943 | . . . . 5 ⊢ (∀𝑥((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵) ↔ (∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵)) | |
4 | 2, 3 | bitr4i 281 | . . . 4 ⊢ ((𝑦 ∈ ∪ 𝐴 → 𝑦 ∈ 𝐵) ↔ ∀𝑥((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵)) |
5 | 4 | albii 1821 | . . 3 ⊢ (∀𝑦(𝑦 ∈ ∪ 𝐴 → 𝑦 ∈ 𝐵) ↔ ∀𝑦∀𝑥((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵)) |
6 | alcom 2160 | . . . 4 ⊢ (∀𝑦∀𝑥((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵) ↔ ∀𝑥∀𝑦((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵)) | |
7 | 19.21v 1940 | . . . . . 6 ⊢ (∀𝑦(𝑥 ∈ 𝐴 → (𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐵)) ↔ (𝑥 ∈ 𝐴 → ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐵))) | |
8 | impexp 454 | . . . . . . . 8 ⊢ (((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵) ↔ (𝑦 ∈ 𝑥 → (𝑥 ∈ 𝐴 → 𝑦 ∈ 𝐵))) | |
9 | bi2.04 392 | . . . . . . . 8 ⊢ ((𝑦 ∈ 𝑥 → (𝑥 ∈ 𝐴 → 𝑦 ∈ 𝐵)) ↔ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐵))) | |
10 | 8, 9 | bitri 278 | . . . . . . 7 ⊢ (((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐵))) |
11 | 10 | albii 1821 | . . . . . 6 ⊢ (∀𝑦((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵) ↔ ∀𝑦(𝑥 ∈ 𝐴 → (𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐵))) |
12 | dfss2 3901 | . . . . . . 7 ⊢ (𝑥 ⊆ 𝐵 ↔ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐵)) | |
13 | 12 | imbi2i 339 | . . . . . 6 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐵) ↔ (𝑥 ∈ 𝐴 → ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐵))) |
14 | 7, 11, 13 | 3bitr4i 306 | . . . . 5 ⊢ (∀𝑦((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐵)) |
15 | 14 | albii 1821 | . . . 4 ⊢ (∀𝑥∀𝑦((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐵)) |
16 | 6, 15 | bitri 278 | . . 3 ⊢ (∀𝑦∀𝑥((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐵)) |
17 | 5, 16 | bitri 278 | . 2 ⊢ (∀𝑦(𝑦 ∈ ∪ 𝐴 → 𝑦 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐵)) |
18 | dfss2 3901 | . 2 ⊢ (∪ 𝐴 ⊆ 𝐵 ↔ ∀𝑦(𝑦 ∈ ∪ 𝐴 → 𝑦 ∈ 𝐵)) | |
19 | df-ral 3111 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐵)) | |
20 | 17, 18, 19 | 3bitr4i 306 | 1 ⊢ (∪ 𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 ∀wal 1536 ∃wex 1781 ∈ wcel 2111 ∀wral 3106 ⊆ wss 3881 ∪ cuni 4800 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-11 2158 ax-ext 2770 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1782 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-ral 3111 df-v 3443 df-in 3888 df-ss 3898 df-uni 4801 |
This theorem is referenced by: uniss2 4833 ssunieq 4835 sspwuni 4985 pwssb 4986 ordunisssuc 6261 sorpssuni 7438 uniordint 7501 sbthlem1 8611 ordunifi 8752 isfinite2 8760 cflim2 9674 fin23lem16 9746 fin23lem29 9752 fin1a2lem11 9821 fin1a2lem13 9823 itunitc 9832 zorng 9915 wuncval2 10158 suplem1pr 10463 suplem2pr 10464 mrcuni 16884 ipodrsfi 17765 mrelatlub 17788 subgint 18295 efgval 18835 toponmre 21698 neips 21718 neiuni 21727 alexsubALTlem2 22653 alexsubALTlem3 22654 tgpconncompeqg 22717 unidmvol 24145 tglnunirn 26342 uniinn0 30314 elrspunidl 31014 ssmxidllem 31049 locfinreflem 31193 zarclsiin 31224 zarclsint 31225 zarcmplem 31234 sxbrsigalem0 31639 dya2iocuni 31651 dya2iocucvr 31652 carsguni 31676 topjoin 33826 fnejoin1 33829 fnejoin2 33830 ovoliunnfl 35099 voliunnfl 35101 volsupnfl 35102 intidl 35467 unichnidl 35469 mnuunid 40985 expanduniss 41001 salexct 42974 setrec1lem2 45218 setrec2fun 45222 |
Copyright terms: Public domain | W3C validator |