Theorem unissb 4871

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 2168. (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 4841	. . . . . 6 ⊢ (𝑦 ∈ ∪ 𝐴 ↔ ∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴))
2	1	imbi1i 350	. . . . 5 ⊢ ((𝑦 ∈ ∪ 𝐴 → 𝑦 ∈ 𝐵) ↔ (∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵))
3		19.23v 1949	. . . . 5 ⊢ (∀𝑥((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵) ↔ (∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵))
4	2, 3	bitr4i 279	. . . 4 ⊢ ((𝑦 ∈ ∪ 𝐴 → 𝑦 ∈ 𝐵) ↔ ∀𝑥((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵))
5	4	albii 1826	. . 3 ⊢ (∀𝑦(𝑦 ∈ ∪ 𝐴 → 𝑦 ∈ 𝐵) ↔ ∀𝑦∀𝑥((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵))
6		elequ1 2126	. . . . . . 7 ⊢ (𝑦 = 𝑧 → (𝑦 ∈ 𝑥 ↔ 𝑧 ∈ 𝑥))
7	6	anbi1d 637	. . . . . 6 ⊢ (𝑦 = 𝑧 → ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) ↔ (𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴)))
8		eleq1w 2822	. . . . . 6 ⊢ (𝑦 = 𝑧 → (𝑦 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵))
9	7, 8	imbi12d 345	. . . . 5 ⊢ (𝑦 = 𝑧 → (((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵) ↔ ((𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑧 ∈ 𝐵)))
10		elequ2 2134	. . . . . . 7 ⊢ (𝑥 = 𝑧 → (𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝑧))
11		eleq1w 2822	. . . . . . 7 ⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴))
12	10, 11	anbi12d 638	. . . . . 6 ⊢ (𝑥 = 𝑧 → ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) ↔ (𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝐴)))
13	12	imbi1d 342	. . . . 5 ⊢ (𝑥 = 𝑧 → (((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵) ↔ ((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝐴) → 𝑦 ∈ 𝐵)))
14	9, 13	alcomw 2052	. . . 4 ⊢ (∀𝑦∀𝑥((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵) ↔ ∀𝑥∀𝑦((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵))
15		19.21v 1946	. . . . . 6 ⊢ (∀𝑦(𝑥 ∈ 𝐴 → (𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐵)) ↔ (𝑥 ∈ 𝐴 → ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐵)))
16		impexp 451	. . . . . . . 8 ⊢ (((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵) ↔ (𝑦 ∈ 𝑥 → (𝑥 ∈ 𝐴 → 𝑦 ∈ 𝐵)))
17		bi2.04 388	. . . . . . . 8 ⊢ ((𝑦 ∈ 𝑥 → (𝑥 ∈ 𝐴 → 𝑦 ∈ 𝐵)) ↔ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐵)))
18	16, 17	bitri 276	. . . . . . 7 ⊢ (((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐵)))
19	18	albii 1826	. . . . . 6 ⊢ (∀𝑦((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵) ↔ ∀𝑦(𝑥 ∈ 𝐴 → (𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐵)))
20		df-ss 3900	. . . . . . 7 ⊢ (𝑥 ⊆ 𝐵 ↔ ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐵))
21	20	imbi2i 337	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐵) ↔ (𝑥 ∈ 𝐴 → ∀𝑦(𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐵)))
22	15, 19, 21	3bitr4i 304	. . . . 5 ⊢ (∀𝑦((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐵))
23	22	albii 1826	. . . 4 ⊢ (∀𝑥∀𝑦((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐵))
24	14, 23	bitri 276	. . 3 ⊢ (∀𝑦∀𝑥((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴) → 𝑦 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐵))
25	5, 24	bitri 276	. 2 ⊢ (∀𝑦(𝑦 ∈ ∪ 𝐴 → 𝑦 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐵))
26		df-ss 3900	. 2 ⊢ (∪ 𝐴 ⊆ 𝐵 ↔ ∀𝑦(𝑦 ∈ ∪ 𝐴 → 𝑦 ∈ 𝐵))
27		df-ral 3054	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐵))
28	25, 26, 27	3bitr4i 304	1 ⊢ (∪ 𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵)

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396  ∀wal 1545  ∃wex 1786   ∈ wcel 2119  ∀wral 3053   ⊆ wss 3883  ∪ cuni 4838

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054  df-v 3433  df-ss 3900  df-uni 4839

This theorem is referenced by:  uniss2  4872  ssunieq  4874  sspwuni  5029  pwssb  5030  ordunisssuc  6418  sorpssuni  7675  uniordint  7744  sbthlem1  9015  ordunifi  9190  isfinite2  9198  cflim2  10176  fin23lem16  10248  fin23lem29  10254  fin1a2lem11  10323  fin1a2lem13  10325  itunitc  10334  zorng  10417  wuncval2  10661  suplem1pr  10966  suplem2pr  10967  mrcuni  17578  ipodrsfi  18496  mrelatlub  18519  subgint  19117  efgval  19683  toponmre  23076  neips  23096  neiuni  23105  alexsubALTlem2  24031  alexsubALTlem3  24032  tgpconncompeqg  24095  unidmvol  25526  oldf  27847  tglnunirn  28634  uniinn0  32639  elrspunidl  33511  ssdifidllem  33539  ssmxidllem  33556  locfinreflem  34024  zarclsiin  34055  zarclsint  34056  zarcmplem  34065  sxbrsigalem0  34455  dya2iocuni  34467  dya2iocucvr  34468  carsguni  34492  topjoin  36593  fnejoin1  36596  fnejoin2  36597  ovoliunnfl  38029  voliunnfl  38031  volsupnfl  38032  intidl  38396  unichnidl  38398  onuniintrab  43671  onsupmaxb  43684  onsupnub  43694  mnuunid  44721  expanduniss  44737  salexct  46777  unilbss  49308  unilbeu  49475  ipolublem  49476  setrec1lem2  50178  setrec2fun  50182