Theorem iunss 4988

Description: Subset theorem for an indexed union. (Contributed by NM, 13-Sep-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) Avoid ax-10 2147, ax-12 2185. (Revised by SN, 2-Feb-2026.)

Assertion

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

Distinct variable group:   𝑥,𝐶

Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)

Proof of Theorem iunss

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-ss 3907	. 2 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑦(𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → 𝑦 ∈ 𝐶))
2		eliun 4938	. . . 4 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)
3	2	imbi1i 349	. . 3 ⊢ ((𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → 𝑦 ∈ 𝐶) ↔ (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
4	3	albii 1821	. 2 ⊢ (∀𝑦(𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
5		df-ss 3907	. . . 4 ⊢ (𝐵 ⊆ 𝐶 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
6	5	ralbii 3084	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
7		ralcom4 3264	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑦∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
8		r19.23v 3165	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
9	8	albii 1821	. . 3 ⊢ (∀𝑦∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
10	6, 7, 9	3bitrri 298	. 2 ⊢ (∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶)
11	1, 4, 10	3bitri 297	1 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶)

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1540   ∈ wcel 2114  ∀wral 3052  ∃wrex 3062   ⊆ wss 3890  ∪ ciun 4934

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-11 2163  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-v 3432  df-ss 3907  df-iun 4936

This theorem is referenced by:  iunss2  4993  iunssd  4994  reliun  5767  djussxp  5796  fiun  7891  f1iun  7892  frrlem7  8237  onfununi  8276  oawordeulem  8484  oaabslem  8578  oaabs2  8580  omabslem  8581  omabs  8582  marypha2lem1  9343  ttrclselem1  9641  trcl  9644  r1val1  9705  rankuni2b  9772  rankval4  9786  rankbnd  9787  rankbnd2  9788  rankc1  9789  cfslb2n  10185  cfsmolem  10187  hsmexlem2  10344  axdc3lem2  10368  ac6  10397  wuncval2  10665  inar1  10693  tskuni  10701  grur1a  10737  fsuppmapnn0fiublem  13947  fsuppmapnn0fiub  13948  rtrclreclem4  15018  prmreclem4  16885  prmreclem5  16886  prdsval  17413  prdsbas  17415  imasaddfnlem  17487  imasvscafn  17496  imasvscaf  17498  isacs2  17614  mreacs  17619  acsfn  17620  dmcoass  18028  isacs5  18509  dprdspan  19999  dprd2dlem1  20013  dprd2d2  20016  dmdprdsplit2lem  20017  lbsextlem2  21153  lpival  21318  iunocv  21675  tgidm  22959  iunconn  23407  comppfsc  23511  txtube  23619  txcmplem2  23621  xkococnlem  23638  xkoinjcn  23666  alexsubALTlem3  24028  cnextf  24045  imasdsf1olem  24352  metnrmlem3  24841  ovolfiniun  25482  ovoliunlem2  25484  ovoliun  25486  ovoliunnul  25488  volfiniun  25528  voliunlem1  25531  volsup  25537  uniioombllem3a  25565  uniioombllem3  25566  uniioombllem4  25567  ismbf3d  25635  limciun  25875  taylfval  26339  taylf  26341  bdayle  27926  elpwiuncl  32616  disjunsn  32683  gsumpart  33143  esum2d  34257  omssubadd  34464  eulerpartlemgh  34542  eulerpartlemgs2  34544  bnj226  34897  bnj517  35047  bnj1118  35146  bnj1137  35157  rankval4b  35263  tz9.1regs  35298  cvmlift2lem12  35516  ntruni  36529  neibastop2lem  36562  filnetlem4  36583  ttciunun  36713  mblfinlem2  37997  volsupnfl  38004  cnambfre  38007  sstotbnd2  38113  equivtotbnd  38117  totbndbnd  38128  prdstotbnd  38133  heiborlem1  38150  pclfinN  40364  lcfrlem4  42009  lcfrlem16  42022  lcfr  42049  oaabsb  43744  naddgeoa  43844  naddwordnexlem4  43851  iunrelexp0  44151  iunrelexpmin1  44157  iunrelexpmin2  44161  cotrcltrcl  44174  trclimalb2  44175  cotrclrcl  44191  iunconnlem2  45383  ixpssmapc  45526  ioorrnopnlem  46754  omeiunle  46967  omeiunltfirp  46969  carageniuncl  46973  caratheodorylem1  46976  caratheodorylem2  46977  hoissrrn  46999  ovnlecvr  47008  ovnsubaddlem1  47020  ovnsubadd  47022  hoissrrn2  47028  ovnlecvr2  47060  hspmbl  47079  opnvonmbllem2  47083  vonvolmbllem  47110  vonvolmbl2  47113  vonvol2  47114  iunhoiioolem  47125  iunhoiioo  47126  iuneq0  49310  iuneqconst2  49314  imassc  49644