Theorem iunss 5003

Description: Subset theorem for an indexed union. (Contributed by NM, 13-Sep-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) Avoid ax-10 2178, 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 3916	. 2 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑦(𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → 𝑦 ∈ 𝐶))
2		eliun 4955	. . . 4 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)
3	2	imbi1i 352	. . 3 ⊢ ((𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → 𝑦 ∈ 𝐶) ↔ (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
4	3	albii 1852	. 2 ⊢ (∀𝑦(𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
5		df-ss 3916	. . . 4 ⊢ (𝐵 ⊆ 𝐶 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
6	5	ralbii 3109	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
7		ralcom4 3289	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑦∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
8		r19.23v 3190	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
9	8	albii 1852	. . 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 2145  ∀wral 3077  ∃wrex 3087   ⊆ wss 3899  ∪ ciun 4951

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-11 2194  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-v 3453  df-ss 3916  df-iun 4953

This theorem is used by:  iunss2  5008  iunssd  5009  reliun  5794  djussxp  5823  fiun  7955  f1iun  7956  frrlem7  8310  onfununi  8349  oawordeulem  8562  oaabslem  8656  oaabs2  8658  omabslem  8659  omabs  8660  marypha2lem1  9427  ttrclselem1  9726  trcl  9729  r1val1  9793  rankuni2b  9867  rankval4b  9880  rankval4  9884  rankbnd  9885  rankbnd2  9886  rankc1  9887  cfslb2n  10346  cfsmolem  10348  hsmexlem2  10505  axdc3lem2  10529  ac6  10558  wuncval2  10832  inar1  10860  tskuni  10868  grur1a  10904  fsuppmapnn0fiublem  14133  fsuppmapnn0fiub  14134  rtrclreclem4  15214  prmreclem4  17097  prmreclem5  17098  prdsval  17626  prdsbas  17628  imasaddfnlem  17700  imasvscafn  17709  imasvscaf  17711  isacs2  17827  mreacs  17832  acsfn  17833  dmcoass  18241  isacs5  18722  dprdspan  20243  dprd2dlem1  20257  dprd2d2  20260  dmdprdsplit2lem  20261  lbsextlem2  21437  lpival  21648  iunocv  21987  tgidm  23298  iunconn  23746  comppfsc  23851  txtube  23959  txcmplem2  23961  xkococnlem  23978  xkoinjcn  24006  alexsubALTlem3  24368  cnextf  24385  imasdsf1olem  24692  metnrmlem3  25181  ovolfiniun  25822  ovoliunlem2  25824  ovoliun  25826  ovoliunnul  25828  volfiniun  25868  voliunlem1  25871  volsup  25877  uniioombllem3a  25905  uniioombllem3  25906  uniioombllem4  25907  ismbf3d  25975  limciun  26214  taylfval  26686  taylf  26688  bdayle  28302  elpwiuncl  33123  disjunsn  33188  gsumpart  33624  esum2d  34725  omssubadd  34932  eulerpartlemgh  35010  eulerpartlemgs2  35012  bnj226  35365  bnj517  35515  bnj1118  35614  bnj1137  35625  tz9.1regs  35802  cvmlift2lem12  36079  ntruni  37115  neibastop2lem  37148  filnetlem4  37169  ttciunun  37299  mblfinlem2  38576  volsupnfl  38583  cnambfre  38586  sstotbnd2  38708  equivtotbnd  38712  totbndbnd  38723  prdstotbnd  38728  heiborlem1  38745  pclfinN  40957  lcfrlem4  42602  lcfrlem16  42615  lcfr  42642  oaabsb  44295  naddgeoa  44395  naddwordnexlem4  44402  iunrelexp0  44701  iunrelexpmin1  44707  iunrelexpmin2  44711  cotrcltrcl  44724  trclimalb2  44725  cotrclrcl  44741  iunconnlem2  45916  ixpssmapc  46089  ioorrnopnlem  47313  omeiunle  47526  omeiunltfirp  47528  carageniuncl  47532  caratheodorylem1  47535  caratheodorylem2  47536  hoissrrn  47558  ovnlecvr  47567  ovnsubaddlem1  47579  ovnsubadd  47581  hoissrrn2  47587  ovnlecvr2  47619  hspmbl  47638  opnvonmbllem2  47642  vonvolmbllem  47669  vonvolmbl2  47672  vonvol2  47673  iunhoiioolem  47684  iunhoiioo  47685  iuneq0  49928  iuneqconst2  49932  imassc  50260