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 2177, ax-12 2212. (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 3896	. 2 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑦(𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → 𝑦 ∈ 𝐶))
2		eliun 4954	. . . 4 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)
3	2	imbi1i 352	. . 3 ⊢ ((𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → 𝑦 ∈ 𝐶) ↔ (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
4	3	albii 1851	. 2 ⊢ (∀𝑦(𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
5		df-ss 3896	. . . 4 ⊢ (𝐵 ⊆ 𝐶 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
6	5	ralbii 3108	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
7		ralcom4 3288	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑦∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
8		r19.23v 3189	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
9	8	albii 1851	. . 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 1567   ∈ wcel 2144  ∀wral 3076  ∃wrex 3086   ⊆ wss 3895  ∪ ciun 4950

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-11 2193  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-v 3452  df-ss 3896  df-iun 4952

This theorem is used by:  iunss2  5007  iunssd  5008  reliun  5793  djussxp  5822  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  33165  disjunsn  33230  gsumpart  33666  esum2d  34767  omssubadd  34974  eulerpartlemgh  35052  eulerpartlemgs2  35054  bnj226  35407  bnj517  35557  bnj1118  35656  bnj1137  35667  tz9.1regs  35844  cvmlift2lem12  36121  ntruni  37157  neibastop2lem  37190  filnetlem4  37211  ttciunun  37341  mblfinlem2  38619  volsupnfl  38626  cnambfre  38629  sstotbnd2  38751  equivtotbnd  38755  totbndbnd  38766  prdstotbnd  38771  heiborlem1  38788  pclfinN  41000  lcfrlem4  42645  lcfrlem16  42658  lcfr  42685  oaabsb  44338  naddgeoa  44438  naddwordnexlem4  44445  iunrelexp0  44744  iunrelexpmin1  44750  iunrelexpmin2  44754  cotrcltrcl  44767  trclimalb2  44768  cotrclrcl  44784  iunconnlem2  45959  ixpssmapc  46132  ioorrnopnlem  47356  omeiunle  47569  omeiunltfirp  47571  carageniuncl  47575  caratheodorylem1  47578  caratheodorylem2  47579  hoissrrn  47601  ovnlecvr  47610  ovnsubaddlem1  47622  ovnsubadd  47624  hoissrrn2  47630  ovnlecvr2  47662  hspmbl  47681  opnvonmbllem2  47685  vonvolmbllem  47712  vonvolmbl2  47715  vonvol2  47716  iunhoiioolem  47727  iunhoiioo  47728  iuneq0  49971  iuneqconst2  49975  imassc  50303