Theorem unissb 4903

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 2158. (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 4874	. . . . . 6 ⊢ (𝑦 ∈ ∪ 𝐴 ↔ ∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴))
2	1	imbi1i 349	. . . . 5 ⊢ ((𝑦 ∈ ∪ 𝐴 → 𝑦 ∈ 𝐵) ↔ (∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵))
3		19.23v 1942	. . . . 5 ⊢ (∀𝑥((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵) ↔ (∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵))
4	2, 3	bitr4i 278	. . . 4 ⊢ ((𝑦 ∈ ∪ 𝐴 → 𝑦 ∈ 𝐵) ↔ ∀𝑥((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵))
5	4	albii 1819	. . 3 ⊢ (∀𝑦(𝑦 ∈ ∪ 𝐴 → 𝑦 ∈ 𝐵) ↔ ∀𝑦∀𝑥((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵))
6		elequ1 2116	. . . . . . 7 ⊢ (𝑦 = 𝑧 → (𝑦 ∈ 𝑥 ↔ 𝑧 ∈ 𝑥))
7	6	anbi1d 631	. . . . . 6 ⊢ (𝑦 = 𝑧 → ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) ↔ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴)))
8		eleq1w 2811	. . . . . 6 ⊢ (𝑦 = 𝑧 → (𝑦 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵))
9	7, 8	imbi12d 344	. . . . 5 ⊢ (𝑦 = 𝑧 → (((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵) ↔ ((𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑧 ∈ 𝐵)))
10		elequ2 2124	. . . . . . 7 ⊢ (𝑥 = 𝑧 → (𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝑧))
11		eleq1w 2811	. . . . . . 7 ⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴))
12	10, 11	anbi12d 632	. . . . . 6 ⊢ (𝑥 = 𝑧 → ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) ↔ (𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝐴)))
13	12	imbi1d 341	. . . . 5 ⊢ (𝑥 = 𝑧 → (((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵) ↔ ((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝐴) → 𝑦 ∈ 𝐵)))
14	9, 13	alcomw 2045	. . . 4 ⊢ (∀𝑦∀𝑥((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵) ↔ ∀𝑥∀𝑦((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵))
15		19.21v 1939	. . . . . 6 ⊢ (∀𝑦(𝑥 ∈ 𝐴 → (𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐵)) ↔ (𝑥 ∈ 𝐴 → ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐵)))
16		impexp 450	. . . . . . . 8 ⊢ (((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵) ↔ (𝑦 ∈ 𝑥 → (𝑥 ∈ 𝐴 → 𝑦 ∈ 𝐵)))
17		bi2.04 387	. . . . . . . 8 ⊢ ((𝑦 ∈ 𝑥 → (𝑥 ∈ 𝐴 → 𝑦 ∈ 𝐵)) ↔ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐵)))
18	16, 17	bitri 275	. . . . . . 7 ⊢ (((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐵)))
19	18	albii 1819	. . . . . 6 ⊢ (∀𝑦((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵) ↔ ∀𝑦(𝑥 ∈ 𝐴 → (𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐵)))
20		df-ss 3931	. . . . . . 7 ⊢ (𝑥 ⊆ 𝐵 ↔ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐵))
21	20	imbi2i 336	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐵) ↔ (𝑥 ∈ 𝐴 → ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐵)))
22	15, 19, 21	3bitr4i 303	. . . . 5 ⊢ (∀𝑦((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐵))
23	22	albii 1819	. . . 4 ⊢ (∀𝑥∀𝑦((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐵))
24	14, 23	bitri 275	. . 3 ⊢ (∀𝑦∀𝑥((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐵))
25	5, 24	bitri 275	. 2 ⊢ (∀𝑦(𝑦 ∈ ∪ 𝐴 → 𝑦 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐵))
26		df-ss 3931	. 2 ⊢ (∪ 𝐴 ⊆ 𝐵 ↔ ∀𝑦(𝑦 ∈ ∪ 𝐴 → 𝑦 ∈ 𝐵))
27		df-ral 3045	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐵))
28	25, 26, 27	3bitr4i 303	1 ⊢ (∪ 𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1538  ∃wex 1779   ∈ wcel 2109  ∀wral 3044   ⊆ wss 3914  ∪ cuni 4871

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-v 3449  df-ss 3931  df-uni 4872

This theorem is referenced by:  uniss2  4905  ssunieq  4907  sspwuni  5064  pwssb  5065  ordunisssuc  6440  sorpssuni  7708  uniordint  7777  sbthlem1  9051  ordunifi  9237  isfinite2  9245  cflim2  10216  fin23lem16  10288  fin23lem29  10294  fin1a2lem11  10363  fin1a2lem13  10365  itunitc  10374  zorng  10457  wuncval2  10700  suplem1pr  11005  suplem2pr  11006  mrcuni  17582  ipodrsfi  18498  mrelatlub  18521  subgint  19082  efgval  19647  toponmre  22980  neips  23000  neiuni  23009  alexsubALTlem2  23935  alexsubALTlem3  23936  tgpconncompeqg  23999  unidmvol  25442  oldf  27765  tglnunirn  28475  uniinn0  32479  elrspunidl  33399  ssdifidllem  33427  ssmxidllem  33444  locfinreflem  33830  zarclsiin  33861  zarclsint  33862  zarcmplem  33871  sxbrsigalem0  34262  dya2iocuni  34274  dya2iocucvr  34275  carsguni  34299  topjoin  36353  fnejoin1  36356  fnejoin2  36357  ovoliunnfl  37656  voliunnfl  37658  volsupnfl  37659  intidl  38023  unichnidl  38025  onuniintrab  43215  onsupmaxb  43228  onsupnub  43238  mnuunid  44266  expanduniss  44282  salexct  46332  unilbss  48806  unilbeu  48973  ipolublem  48974  setrec1lem2  49677  setrec2fun  49681