Theorem iunss 4975

Description: Subset theorem for an indexed union. (Contributed by NM, 13-Sep-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) Avoid ax-10 2152, ax-12 2189. (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 3900	. 2 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑦(𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → 𝑦 ∈ 𝐶))
2		eliun 4926	. . . 4 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)
3	2	imbi1i 350	. . 3 ⊢ ((𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → 𝑦 ∈ 𝐶) ↔ (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
4	3	albii 1826	. 2 ⊢ (∀𝑦(𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
5		df-ss 3900	. . . 4 ⊢ (𝐵 ⊆ 𝐶 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
6	5	ralbii 3085	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
7		ralcom4 3265	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑦∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
8		r19.23v 3166	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
9	8	albii 1826	. . 3 ⊢ (∀𝑦∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
10	6, 7, 9	3bitrri 299	. 2 ⊢ (∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶)
11	1, 4, 10	3bitri 298	1 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶)

Syntax hints:   → wi 4   ↔ wb 207  ∀wal 1545   ∈ wcel 2119  ∀wral 3053  ∃wrex 3063   ⊆ wss 3883  ∪ ciun 4922

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-11 2168  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054  df-rex 3064  df-v 3433  df-ss 3900  df-iun 4924

This theorem is referenced by:  iunss2  4980  iunssd  4981  reliun  5760  djussxp  5788  fiun  7886  f1iun  7887  frrlem7  8233  onfununi  8272  oawordeulem  8480  oaabslem  8574  oaabs2  8576  omabslem  8577  omabs  8578  marypha2lem1  9339  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  13944  fsuppmapnn0fiub  13945  rtrclreclem4  15015  prmreclem4  16882  prmreclem5  16883  prdsval  17410  prdsbas  17412  imasaddfnlem  17484  imasvscafn  17493  imasvscaf  17495  isacs2  17611  mreacs  17616  acsfn  17617  dmcoass  18025  isacs5  18506  dprdspan  19996  dprd2dlem1  20010  dprd2d2  20013  dmdprdsplit2lem  20014  lbsextlem2  21153  lpival  21318  iunocv  21657  tgidm  22964  iunconn  23412  comppfsc  23516  txtube  23624  txcmplem2  23626  xkococnlem  23643  xkoinjcn  23671  alexsubALTlem3  24033  cnextf  24050  imasdsf1olem  24357  metnrmlem3  24846  ovolfiniun  25487  ovoliunlem2  25489  ovoliun  25491  ovoliunnul  25493  volfiniun  25533  voliunlem1  25536  volsup  25542  uniioombllem3a  25570  uniioombllem3  25571  uniioombllem4  25572  ismbf3d  25640  limciun  25880  taylfval  26343  taylf  26345  bdayle  27927  elpwiuncl  32616  disjunsn  32684  gsumpart  33145  esum2d  34286  omssubadd  34493  eulerpartlemgh  34571  eulerpartlemgs2  34573  bnj226  34926  bnj517  35076  bnj1118  35175  bnj1137  35186  rankval4b  35290  tz9.1regs  35324  cvmlift2lem12  35551  ntruni  36564  neibastop2lem  36597  filnetlem4  36618  ttciunun  36748  mblfinlem2  38034  volsupnfl  38041  cnambfre  38044  sstotbnd2  38150  equivtotbnd  38154  totbndbnd  38165  prdstotbnd  38170  heiborlem1  38187  pclfinN  40401  lcfrlem4  42046  lcfrlem16  42059  lcfr  42086  oaabsb  43748  naddgeoa  43848  naddwordnexlem4  43855  iunrelexp0  44155  iunrelexpmin1  44161  iunrelexpmin2  44165  cotrcltrcl  44178  trclimalb2  44179  cotrclrcl  44195  iunconnlem2  45387  ixpssmapc  45530  ioorrnopnlem  46755  omeiunle  46968  omeiunltfirp  46970  carageniuncl  46974  caratheodorylem1  46977  caratheodorylem2  46978  hoissrrn  47000  ovnlecvr  47009  ovnsubaddlem1  47021  ovnsubadd  47023  hoissrrn2  47029  ovnlecvr2  47061  hspmbl  47080  opnvonmbllem2  47084  vonvolmbllem  47111  vonvolmbl2  47114  vonvol2  47115  iunhoiioolem  47126  iunhoiioo  47127  iuneq0  49317  iuneqconst2  49321  imassc  49651