Theorem iunss 5013

Description: Subset theorem for an indexed union. (Contributed by NM, 13-Sep-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) Avoid ax-10 2182, ax-12 2219. (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 3930	. 2 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑦(𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → 𝑦 ∈ 𝐶))
2		eliun 4964	. . . 4 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)
3	2	imbi1i 352	. . 3 ⊢ ((𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → 𝑦 ∈ 𝐶) ↔ (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
4	3	albii 1846	. 2 ⊢ (∀𝑦(𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
5		df-ss 3930	. . . 4 ⊢ (𝐵 ⊆ 𝐶 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
6	5	ralbii 3117	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
7		ralcom4 3297	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑦∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
8		r19.23v 3198	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
9	8	albii 1846	. . 3 ⊢ (∀𝑦∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
10	6, 7, 9	3bitrri 301	. 2 ⊢ (∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶)
11	1, 4, 10	3bitri 300	1 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶)

Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1565   ∈ wcel 2149  ∀wral 3085  ∃wrex 3095   ⊆ wss 3913  ∪ ciun 4960

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-11 2198  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-rex 3096  df-v 3465  df-ss 3930  df-iun 4962

This theorem is referenced by:  iunss2  5018  iunssd  5019  reliun  5804  djussxp  5832  fiun  7940  f1iun  7941  frrlem7  8289  onfununi  8328  oawordeulem  8539  oaabslem  8633  oaabs2  8635  omabslem  8636  omabs  8637  marypha2lem1  9395  ttrclselem1  9694  trcl  9697  r1val1  9758  rankuni2b  9825  rankval4  9839  rankbnd  9840  rankbnd2  9841  rankc1  9842  cfslb2n  10252  cfsmolem  10254  hsmexlem2  10411  axdc3lem2  10435  ac6  10464  wuncval2  10732  inar1  10760  tskuni  10768  grur1a  10804  fsuppmapnn0fiublem  14026  fsuppmapnn0fiub  14027  rtrclreclem4  15098  prmreclem4  16979  prmreclem5  16980  prdsval  17508  prdsbas  17510  imasaddfnlem  17582  imasvscafn  17591  imasvscaf  17593  isacs2  17709  mreacs  17714  acsfn  17715  dmcoass  18123  isacs5  18604  dprdspan  20099  dprd2dlem1  20113  dprd2d2  20116  dmdprdsplit2lem  20117  lbsextlem2  21261  lpival  21461  iunocv  21800  tgidm  23106  iunconn  23554  comppfsc  23658  txtube  23766  txcmplem2  23768  xkococnlem  23785  xkoinjcn  23813  alexsubALTlem3  24175  cnextf  24192  imasdsf1olem  24499  metnrmlem3  24988  ovolfiniun  25629  ovoliunlem2  25631  ovoliun  25633  ovoliunnul  25635  volfiniun  25675  voliunlem1  25678  volsup  25684  uniioombllem3a  25712  uniioombllem3  25713  uniioombllem4  25714  ismbf3d  25782  limciun  26022  taylfval  26488  taylf  26490  bdayle  28075  elpwiuncl  32814  disjunsn  32880  gsumpart  33324  esum2d  34428  omssubadd  34635  eulerpartlemgh  34713  eulerpartlemgs2  34715  bnj226  35068  bnj517  35218  bnj1118  35317  bnj1137  35328  rankval4b  35436  tz9.1regs  35480  cvmlift2lem12  35739  ntruni  36761  neibastop2lem  36794  filnetlem4  36815  ttciunun  36945  mblfinlem2  38231  volsupnfl  38238  cnambfre  38241  sstotbnd2  38347  equivtotbnd  38351  totbndbnd  38362  prdstotbnd  38367  heiborlem1  38384  pclfinN  40598  lcfrlem4  42243  lcfrlem16  42256  lcfr  42283  oaabsb  43947  naddgeoa  44047  naddwordnexlem4  44054  iunrelexp0  44354  iunrelexpmin1  44360  iunrelexpmin2  44364  cotrcltrcl  44377  trclimalb2  44378  cotrclrcl  44394  iunconnlem2  45569  ixpssmapc  45719  ioorrnopnlem  46944  omeiunle  47157  omeiunltfirp  47159  carageniuncl  47163  caratheodorylem1  47166  caratheodorylem2  47167  hoissrrn  47189  ovnlecvr  47198  ovnsubaddlem1  47210  ovnsubadd  47212  hoissrrn2  47218  ovnlecvr2  47250  hspmbl  47269  opnvonmbllem2  47273  vonvolmbllem  47300  vonvolmbl2  47303  vonvol2  47304  iunhoiioolem  47315  iunhoiioo  47316  iuneq0  49516  iuneqconst2  49520  imassc  49850