Theorem unissb 4889

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 2160. (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 4859	. . . . . 6 ⊢ (𝑦 ∈ ∪ 𝐴 ↔ ∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴))
2	1	imbi1i 349	. . . . 5 ⊢ ((𝑦 ∈ ∪ 𝐴 → 𝑦 ∈ 𝐵) ↔ (∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵))
3		19.23v 1943	. . . . 5 ⊢ (∀𝑥((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵) ↔ (∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵))
4	2, 3	bitr4i 278	. . . 4 ⊢ ((𝑦 ∈ ∪ 𝐴 → 𝑦 ∈ 𝐵) ↔ ∀𝑥((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵))
5	4	albii 1820	. . 3 ⊢ (∀𝑦(𝑦 ∈ ∪ 𝐴 → 𝑦 ∈ 𝐵) ↔ ∀𝑦∀𝑥((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵))
6		elequ1 2118	. . . . . . 7 ⊢ (𝑦 = 𝑧 → (𝑦 ∈ 𝑥 ↔ 𝑧 ∈ 𝑥))
7	6	anbi1d 631	. . . . . 6 ⊢ (𝑦 = 𝑧 → ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) ↔ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴)))
8		eleq1w 2814	. . . . . 6 ⊢ (𝑦 = 𝑧 → (𝑦 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵))
9	7, 8	imbi12d 344	. . . . 5 ⊢ (𝑦 = 𝑧 → (((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵) ↔ ((𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑧 ∈ 𝐵)))
10		elequ2 2126	. . . . . . 7 ⊢ (𝑥 = 𝑧 → (𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝑧))
11		eleq1w 2814	. . . . . . 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 3914	. . . . . . 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 3914	. 2 ⊢ (∪ 𝐴 ⊆ 𝐵 ↔ ∀𝑦(𝑦 ∈ ∪ 𝐴 → 𝑦 ∈ 𝐵))
27		df-ral 3048	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐵))
28	25, 26, 27	3bitr4i 303	1 ⊢ (∪ 𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1539  ∃wex 1780   ∈ wcel 2111  ∀wral 3047   ⊆ wss 3897  ∪ cuni 4856

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 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-v 3438  df-ss 3914  df-uni 4857

This theorem is referenced by:  uniss2  4890  ssunieq  4892  sspwuni  5046  pwssb  5047  ordunisssuc  6414  sorpssuni  7665  uniordint  7734  sbthlem1  9000  ordunifi  9174  isfinite2  9182  cflim2  10154  fin23lem16  10226  fin23lem29  10232  fin1a2lem11  10301  fin1a2lem13  10303  itunitc  10312  zorng  10395  wuncval2  10638  suplem1pr  10943  suplem2pr  10944  mrcuni  17527  ipodrsfi  18445  mrelatlub  18468  subgint  19063  efgval  19629  toponmre  23008  neips  23028  neiuni  23037  alexsubALTlem2  23963  alexsubALTlem3  23964  tgpconncompeqg  24027  unidmvol  25469  oldf  27798  tglnunirn  28526  uniinn0  32530  elrspunidl  33393  ssdifidllem  33421  ssmxidllem  33438  locfinreflem  33853  zarclsiin  33884  zarclsint  33885  zarcmplem  33894  sxbrsigalem0  34284  dya2iocuni  34296  dya2iocucvr  34297  carsguni  34321  topjoin  36409  fnejoin1  36412  fnejoin2  36413  ovoliunnfl  37712  voliunnfl  37714  volsupnfl  37715  intidl  38079  unichnidl  38081  onuniintrab  43329  onsupmaxb  43342  onsupnub  43352  mnuunid  44380  expanduniss  44396  salexct  46442  unilbss  48928  unilbeu  49095  ipolublem  49096  setrec1lem2  49799  setrec2fun  49803