Theorem unissb 4893

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 2162. (Revised by BTernaryTau, 28-Dec-2024.)

Assertion

Ref	Expression
unissb	⊢ (∪ 𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem unissb

Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eluni 4863	. . . . . 6 ⊢ (𝑦 ∈ ∪ 𝐴 ↔ ∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴))
2	1	imbi1i 349	. . . . 5 ⊢ ((𝑦 ∈ ∪ 𝐴 → 𝑦 ∈ 𝐵) ↔ (∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵))
3		19.23v 1943	. . . . 5 ⊢ (∀𝑥((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵) ↔ (∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵))
4	2, 3	bitr4i 278	. . . 4 ⊢ ((𝑦 ∈ ∪ 𝐴 → 𝑦 ∈ 𝐵) ↔ ∀𝑥((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵))
5	4	albii 1820	. . 3 ⊢ (∀𝑦(𝑦 ∈ ∪ 𝐴 → 𝑦 ∈ 𝐵) ↔ ∀𝑦∀𝑥((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵))
6		elequ1 2120	. . . . . . 7 ⊢ (𝑦 = 𝑧 → (𝑦 ∈ 𝑥 ↔ 𝑧 ∈ 𝑥))
7	6	anbi1d 631	. . . . . 6 ⊢ (𝑦 = 𝑧 → ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) ↔ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴)))
8		eleq1w 2816	. . . . . 6 ⊢ (𝑦 = 𝑧 → (𝑦 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵))
9	7, 8	imbi12d 344	. . . . 5 ⊢ (𝑦 = 𝑧 → (((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵) ↔ ((𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑧 ∈ 𝐵)))
10		elequ2 2128	. . . . . . 7 ⊢ (𝑥 = 𝑧 → (𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝑧))
11		eleq1w 2816	. . . . . . 7 ⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴))
12	10, 11	anbi12d 632	. . . . . 6 ⊢ (𝑥 = 𝑧 → ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) ↔ (𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝐴)))
13	12	imbi1d 341	. . . . 5 ⊢ (𝑥 = 𝑧 → (((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵) ↔ ((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝐴) → 𝑦 ∈ 𝐵)))
14	9, 13	alcomw 2046	. . . 4 ⊢ (∀𝑦∀𝑥((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵) ↔ ∀𝑥∀𝑦((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵))
15		19.21v 1940	. . . . . 6 ⊢ (∀𝑦(𝑥 ∈ 𝐴 → (𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐵)) ↔ (𝑥 ∈ 𝐴 → ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐵)))
16		impexp 450	. . . . . . . 8 ⊢ (((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵) ↔ (𝑦 ∈ 𝑥 → (𝑥 ∈ 𝐴 → 𝑦 ∈ 𝐵)))
17		bi2.04 387	. . . . . . . 8 ⊢ ((𝑦 ∈ 𝑥 → (𝑥 ∈ 𝐴 → 𝑦 ∈ 𝐵)) ↔ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐵)))
18	16, 17	bitri 275	. . . . . . 7 ⊢ (((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐵)))
19	18	albii 1820	. . . . . 6 ⊢ (∀𝑦((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵) ↔ ∀𝑦(𝑥 ∈ 𝐴 → (𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐵)))
20		df-ss 3915	. . . . . . 7 ⊢ (𝑥 ⊆ 𝐵 ↔ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐵))
21	20	imbi2i 336	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐵) ↔ (𝑥 ∈ 𝐴 → ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐵)))
22	15, 19, 21	3bitr4i 303	. . . . 5 ⊢ (∀𝑦((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐵))
23	22	albii 1820	. . . 4 ⊢ (∀𝑥∀𝑦((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐵))
24	14, 23	bitri 275	. . 3 ⊢ (∀𝑦∀𝑥((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐵))
25	5, 24	bitri 275	. 2 ⊢ (∀𝑦(𝑦 ∈ ∪ 𝐴 → 𝑦 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐵))
26		df-ss 3915	. 2 ⊢ (∪ 𝐴 ⊆ 𝐵 ↔ ∀𝑦(𝑦 ∈ ∪ 𝐴 → 𝑦 ∈ 𝐵))
27		df-ral 3049	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐵))
28	25, 26, 27	3bitr4i 303	1 ⊢ (∪ 𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1539  ∃wex 1780   ∈ wcel 2113  ∀wral 3048   ⊆ wss 3898  ∪ cuni 4860

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ral 3049  df-v 3439  df-ss 3915  df-uni 4861

This theorem is referenced by:  uniss2  4894  ssunieq  4896  sspwuni  5052  pwssb  5053  ordunisssuc  6422  sorpssuni  7674  uniordint  7743  sbthlem1  9011  ordunifi  9185  isfinite2  9193  cflim2  10165  fin23lem16  10237  fin23lem29  10243  fin1a2lem11  10312  fin1a2lem13  10314  itunitc  10323  zorng  10406  wuncval2  10649  suplem1pr  10954  suplem2pr  10955  mrcuni  17535  ipodrsfi  18453  mrelatlub  18476  subgint  19071  efgval  19637  toponmre  23028  neips  23048  neiuni  23057  alexsubALTlem2  23983  alexsubALTlem3  23984  tgpconncompeqg  24047  unidmvol  25489  oldf  27818  tglnunirn  28546  uniinn0  32551  elrspunidl  33437  ssdifidllem  33465  ssmxidllem  33482  locfinreflem  33925  zarclsiin  33956  zarclsint  33957  zarcmplem  33966  sxbrsigalem0  34356  dya2iocuni  34368  dya2iocucvr  34369  carsguni  34393  topjoin  36481  fnejoin1  36484  fnejoin2  36485  ovoliunnfl  37775  voliunnfl  37777  volsupnfl  37778  intidl  38142  unichnidl  38144  onuniintrab  43383  onsupmaxb  43396  onsupnub  43406  mnuunid  44434  expanduniss  44450  salexct  46494  unilbss  48979  unilbeu  49146  ipolublem  49147  setrec1lem2  49849  setrec2fun  49853