Theorem iunss 4987

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 3906	. 2 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑦(𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → 𝑦 ∈ 𝐶))
2		eliun 4937	. . . 4 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)
3	2	imbi1i 349	. . 3 ⊢ ((𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → 𝑦 ∈ 𝐶) ↔ (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
4	3	albii 1821	. 2 ⊢ (∀𝑦(𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
5		df-ss 3906	. . . 4 ⊢ (𝐵 ⊆ 𝐶 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
6	5	ralbii 3083	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
7		ralcom4 3263	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑦∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
8		r19.23v 3164	. . . 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 3051  ∃wrex 3061   ⊆ wss 3889  ∪ ciun 4933

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3062  df-v 3431  df-ss 3906  df-iun 4935

This theorem is referenced by:  iunss2  4992  iunssd  4993  reliun  5772  djussxp  5800  fiun  7896  f1iun  7897  frrlem7  8242  onfununi  8281  oawordeulem  8489  oaabslem  8583  oaabs2  8585  omabslem  8586  omabs  8587  marypha2lem1  9348  ttrclselem1  9646  trcl  9649  r1val1  9710  rankuni2b  9777  rankval4  9791  rankbnd  9792  rankbnd2  9793  rankc1  9794  cfslb2n  10190  cfsmolem  10192  hsmexlem2  10349  axdc3lem2  10373  ac6  10402  wuncval2  10670  inar1  10698  tskuni  10706  grur1a  10742  fsuppmapnn0fiublem  13952  fsuppmapnn0fiub  13953  rtrclreclem4  15023  prmreclem4  16890  prmreclem5  16891  prdsval  17418  prdsbas  17420  imasaddfnlem  17492  imasvscafn  17501  imasvscaf  17503  isacs2  17619  mreacs  17624  acsfn  17625  dmcoass  18033  isacs5  18514  dprdspan  20004  dprd2dlem1  20018  dprd2d2  20021  dmdprdsplit2lem  20022  lbsextlem2  21157  lpival  21322  iunocv  21661  tgidm  22945  iunconn  23393  comppfsc  23497  txtube  23605  txcmplem2  23607  xkococnlem  23624  xkoinjcn  23652  alexsubALTlem3  24014  cnextf  24031  imasdsf1olem  24338  metnrmlem3  24827  ovolfiniun  25468  ovoliunlem2  25470  ovoliun  25472  ovoliunnul  25474  volfiniun  25514  voliunlem1  25517  volsup  25523  uniioombllem3a  25551  uniioombllem3  25552  uniioombllem4  25553  ismbf3d  25621  limciun  25861  taylfval  26324  taylf  26326  bdayle  27908  elpwiuncl  32597  disjunsn  32664  gsumpart  33124  esum2d  34237  omssubadd  34444  eulerpartlemgh  34522  eulerpartlemgs2  34524  bnj226  34877  bnj517  35027  bnj1118  35126  bnj1137  35137  rankval4b  35243  tz9.1regs  35278  cvmlift2lem12  35496  ntruni  36509  neibastop2lem  36542  filnetlem4  36563  ttciunun  36693  mblfinlem2  37979  volsupnfl  37986  cnambfre  37989  sstotbnd2  38095  equivtotbnd  38099  totbndbnd  38110  prdstotbnd  38115  heiborlem1  38132  pclfinN  40346  lcfrlem4  41991  lcfrlem16  42004  lcfr  42031  oaabsb  43722  naddgeoa  43822  naddwordnexlem4  43829  iunrelexp0  44129  iunrelexpmin1  44135  iunrelexpmin2  44139  cotrcltrcl  44152  trclimalb2  44153  cotrclrcl  44169  iunconnlem2  45361  ixpssmapc  45504  ioorrnopnlem  46732  omeiunle  46945  omeiunltfirp  46947  carageniuncl  46951  caratheodorylem1  46954  caratheodorylem2  46955  hoissrrn  46977  ovnlecvr  46986  ovnsubaddlem1  46998  ovnsubadd  47000  hoissrrn2  47006  ovnlecvr2  47038  hspmbl  47057  opnvonmbllem2  47061  vonvolmbllem  47088  vonvolmbl2  47091  vonvol2  47092  iunhoiioolem  47103  iunhoiioo  47104  iuneq0  49294  iuneqconst2  49298  imassc  49628