Theorem iunss 5002

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 3920	. 2 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑦(𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → 𝑦 ∈ 𝐶))
2		eliun 4952	. . . 4 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)
3	2	imbi1i 349	. . 3 ⊢ ((𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → 𝑦 ∈ 𝐶) ↔ (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
4	3	albii 1821	. 2 ⊢ (∀𝑦(𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
5		df-ss 3920	. . . 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 3903  ∪ ciun 4948

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 3444  df-ss 3920  df-iun 4950

This theorem is referenced by:  iunss2  5007  iunssd  5008  reliun  5775  djussxp  5804  fiun  7899  f1iun  7900  frrlem7  8246  onfununi  8285  oawordeulem  8493  oaabslem  8587  oaabs2  8589  omabslem  8590  omabs  8591  marypha2lem1  9352  ttrclselem1  9648  trcl  9651  r1val1  9712  rankuni2b  9779  rankval4  9793  rankbnd  9794  rankbnd2  9795  rankc1  9796  cfslb2n  10192  cfsmolem  10194  hsmexlem2  10351  axdc3lem2  10375  ac6  10404  wuncval2  10672  inar1  10700  tskuni  10708  grur1a  10744  fsuppmapnn0fiublem  13927  fsuppmapnn0fiub  13928  rtrclreclem4  14998  prmreclem4  16861  prmreclem5  16862  prdsval  17389  prdsbas  17391  imasaddfnlem  17463  imasvscafn  17472  imasvscaf  17474  isacs2  17590  mreacs  17595  acsfn  17596  dmcoass  18004  isacs5  18485  dprdspan  19975  dprd2dlem1  19989  dprd2d2  19992  dmdprdsplit2lem  19993  lbsextlem2  21131  lpival  21296  iunocv  21653  tgidm  22941  iunconn  23389  comppfsc  23493  txtube  23601  txcmplem2  23603  xkococnlem  23620  xkoinjcn  23648  alexsubALTlem3  24010  cnextf  24027  imasdsf1olem  24334  metnrmlem3  24823  ovolfiniun  25475  ovoliunlem2  25477  ovoliun  25479  ovoliunnul  25481  volfiniun  25521  voliunlem1  25524  volsup  25530  uniioombllem3a  25558  uniioombllem3  25559  uniioombllem4  25560  ismbf3d  25628  limciun  25868  taylfval  26339  taylf  26341  bdayle  27929  elpwiuncl  32620  disjunsn  32687  gsumpart  33163  esum2d  34277  omssubadd  34484  eulerpartlemgh  34562  eulerpartlemgs2  34564  bnj226  34917  bnj517  35067  bnj1118  35166  bnj1137  35177  rankval4b  35283  tz9.1regs  35318  cvmlift2lem12  35536  ntruni  36549  neibastop2lem  36582  filnetlem4  36603  mblfinlem2  37938  volsupnfl  37945  cnambfre  37948  sstotbnd2  38054  equivtotbnd  38058  totbndbnd  38069  prdstotbnd  38074  heiborlem1  38091  pclfinN  40305  lcfrlem4  41950  lcfrlem16  41963  lcfr  41990  oaabsb  43680  naddgeoa  43780  naddwordnexlem4  43787  iunrelexp0  44087  iunrelexpmin1  44093  iunrelexpmin2  44097  cotrcltrcl  44110  trclimalb2  44111  cotrclrcl  44127  iunconnlem2  45319  ixpssmapc  45462  ioorrnopnlem  46691  omeiunle  46904  omeiunltfirp  46906  carageniuncl  46910  caratheodorylem1  46913  caratheodorylem2  46914  hoissrrn  46936  ovnlecvr  46945  ovnsubaddlem1  46957  ovnsubadd  46959  hoissrrn2  46965  ovnlecvr2  46997  hspmbl  47016  opnvonmbllem2  47020  vonvolmbllem  47047  vonvolmbl2  47050  vonvol2  47051  iunhoiioolem  47062  iunhoiioo  47063  iuneq0  49207  iuneqconst2  49211  imassc  49541