Theorem iunss 5009

Description: Subset theorem for an indexed union. (Contributed by NM, 13-Sep-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) Avoid ax-10 2176, ax-12 2213. (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 3922	. 2 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑦(𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → 𝑦 ∈ 𝐶))
2		eliun 4960	. . . 4 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)
3	2	imbi1i 352	. . 3 ⊢ ((𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → 𝑦 ∈ 𝐶) ↔ (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
4	3	albii 1849	. 2 ⊢ (∀𝑦(𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
5		df-ss 3922	. . . 4 ⊢ (𝐵 ⊆ 𝐶 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
6	5	ralbii 3111	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
7		ralcom4 3291	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑦∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
8		r19.23v 3192	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
9	8	albii 1849	. . 3 ⊢ (∀𝑦∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
10	6, 7, 9	3bitrri 301	. 2 ⊢ (∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶)
11	1, 4, 10	3bitri 300	1 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1568   ∈ wcel 2143  ∀wral 3079  ∃wrex 3089   ⊆ wss 3905  ∪ ciun 4956

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-11 2192  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-v 3457  df-ss 3922  df-iun 4958

This theorem is used by:  iunss2  5014  iunssd  5015  reliun  5803  djussxp  5831  fiun  7936  f1iun  7937  frrlem7  8285  onfununi  8324  oawordeulem  8535  oaabslem  8629  oaabs2  8631  omabslem  8632  omabs  8633  marypha2lem1  9391  ttrclselem1  9690  trcl  9693  r1val1  9754  rankuni2b  9821  rankval4  9835  rankbnd  9836  rankbnd2  9837  rankc1  9838  cfslb2n  10256  cfsmolem  10258  hsmexlem2  10415  axdc3lem2  10439  ac6  10468  wuncval2  10736  inar1  10764  tskuni  10772  grur1a  10808  fsuppmapnn0fiublem  14031  fsuppmapnn0fiub  14032  rtrclreclem4  15103  prmreclem4  16983  prmreclem5  16984  prdsval  17512  prdsbas  17514  imasaddfnlem  17586  imasvscafn  17595  imasvscaf  17597  isacs2  17713  mreacs  17718  acsfn  17719  dmcoass  18127  isacs5  18608  dprdspan  20103  dprd2dlem1  20117  dprd2d2  20120  dmdprdsplit2lem  20121  lbsextlem2  21292  lpival  21501  iunocv  21840  tgidm  23146  iunconn  23594  comppfsc  23698  txtube  23806  txcmplem2  23808  xkococnlem  23825  xkoinjcn  23853  alexsubALTlem3  24215  cnextf  24232  imasdsf1olem  24539  metnrmlem3  25028  ovolfiniun  25669  ovoliunlem2  25671  ovoliun  25673  ovoliunnul  25675  volfiniun  25715  voliunlem1  25718  volsup  25724  uniioombllem3a  25752  uniioombllem3  25753  uniioombllem4  25754  ismbf3d  25822  limciun  26062  taylfval  26531  taylf  26533  bdayle  28118  elpwiuncl  32882  disjunsn  32948  gsumpart  33392  esum2d  34492  omssubadd  34699  eulerpartlemgh  34777  eulerpartlemgs2  34779  bnj226  35132  bnj517  35282  bnj1118  35381  bnj1137  35392  rankval4b  35502  tz9.1regs  35555  cvmlift2lem12  35814  ntruni  36866  neibastop2lem  36899  filnetlem4  36920  ttciunun  37050  mblfinlem2  38337  volsupnfl  38344  cnambfre  38347  sstotbnd2  38453  equivtotbnd  38457  totbndbnd  38468  prdstotbnd  38473  heiborlem1  38490  pclfinN  40702  lcfrlem4  42347  lcfrlem16  42360  lcfr  42387  oaabsb  44049  naddgeoa  44149  naddwordnexlem4  44156  iunrelexp0  44456  iunrelexpmin1  44462  iunrelexpmin2  44466  cotrcltrcl  44479  trclimalb2  44480  cotrclrcl  44496  iunconnlem2  45671  ixpssmapc  45821  ioorrnopnlem  47046  omeiunle  47259  omeiunltfirp  47261  carageniuncl  47265  caratheodorylem1  47268  caratheodorylem2  47269  hoissrrn  47291  ovnlecvr  47300  ovnsubaddlem1  47312  ovnsubadd  47314  hoissrrn2  47320  ovnlecvr2  47352  hspmbl  47371  opnvonmbllem2  47375  vonvolmbllem  47402  vonvolmbl2  47405  vonvol2  47406  iunhoiioolem  47417  iunhoiioo  47418  iuneq0  49625  iuneqconst2  49629  imassc  49959