Theorem iunss 5001

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 3919	. 2 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑦(𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → 𝑦 ∈ 𝐶))
2		eliun 4951	. . . 4 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)
3	2	imbi1i 349	. . 3 ⊢ ((𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → 𝑦 ∈ 𝐶) ↔ (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
4	3	albii 1821	. 2 ⊢ (∀𝑦(𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
5		df-ss 3919	. . . 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 3052  ∃wrex 3061   ⊆ wss 3902  ∪ ciun 4947

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 3062  df-v 3443  df-ss 3919  df-iun 4949

This theorem is referenced by:  iunss2  5006  iunssd  5007  reliun  5766  djussxp  5795  fiun  7889  f1iun  7890  frrlem7  8236  onfununi  8275  oawordeulem  8483  oaabslem  8577  oaabs2  8579  omabslem  8580  omabs  8581  marypha2lem1  9342  ttrclselem1  9638  trcl  9641  r1val1  9702  rankuni2b  9769  rankval4  9783  rankbnd  9784  rankbnd2  9785  rankc1  9786  cfslb2n  10182  cfsmolem  10184  hsmexlem2  10341  axdc3lem2  10365  ac6  10394  wuncval2  10662  inar1  10690  tskuni  10698  grur1a  10734  fsuppmapnn0fiublem  13917  fsuppmapnn0fiub  13918  rtrclreclem4  14988  prmreclem4  16851  prmreclem5  16852  prdsval  17379  prdsbas  17381  imasaddfnlem  17453  imasvscafn  17462  imasvscaf  17464  isacs2  17580  mreacs  17585  acsfn  17586  dmcoass  17994  isacs5  18475  dprdspan  19962  dprd2dlem1  19976  dprd2d2  19979  dmdprdsplit2lem  19980  lbsextlem2  21118  lpival  21283  iunocv  21640  tgidm  22928  iunconn  23376  comppfsc  23480  txtube  23588  txcmplem2  23590  xkococnlem  23607  xkoinjcn  23635  alexsubALTlem3  23997  cnextf  24014  imasdsf1olem  24321  metnrmlem3  24810  ovolfiniun  25462  ovoliunlem2  25464  ovoliun  25466  ovoliunnul  25468  volfiniun  25508  voliunlem1  25511  volsup  25517  uniioombllem3a  25545  uniioombllem3  25546  uniioombllem4  25547  ismbf3d  25615  limciun  25855  taylfval  26326  taylf  26328  bdayle  27916  elpwiuncl  32605  disjunsn  32672  gsumpart  33148  esum2d  34252  omssubadd  34459  eulerpartlemgh  34537  eulerpartlemgs2  34539  bnj226  34892  bnj517  35043  bnj1118  35142  bnj1137  35153  rankval4b  35258  tz9.1regs  35292  cvmlift2lem12  35510  ntruni  36523  neibastop2lem  36556  filnetlem4  36577  mblfinlem2  37861  volsupnfl  37868  cnambfre  37871  sstotbnd2  37977  equivtotbnd  37981  totbndbnd  37992  prdstotbnd  37997  heiborlem1  38014  pclfinN  40228  lcfrlem4  41873  lcfrlem16  41886  lcfr  41913  oaabsb  43603  naddgeoa  43703  naddwordnexlem4  43710  iunrelexp0  44010  iunrelexpmin1  44016  iunrelexpmin2  44020  cotrcltrcl  44033  trclimalb2  44034  cotrclrcl  44050  iunconnlem2  45242  ixpssmapc  45385  ioorrnopnlem  46615  omeiunle  46828  omeiunltfirp  46830  carageniuncl  46834  caratheodorylem1  46837  caratheodorylem2  46838  hoissrrn  46860  ovnlecvr  46869  ovnsubaddlem1  46881  ovnsubadd  46883  hoissrrn2  46889  ovnlecvr2  46921  hspmbl  46940  opnvonmbllem2  46944  vonvolmbllem  46971  vonvolmbl2  46974  vonvol2  46975  iunhoiioolem  46986  iunhoiioo  46987  iuneq0  49131  iuneqconst2  49135  imassc  49465