Theorem iunss 4998

Description: Subset theorem for an indexed union. (Contributed by NM, 13-Sep-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) Avoid ax-10 2146, ax-12 2182. (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 3916	. 2 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑦(𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → 𝑦 ∈ 𝐶))
2		eliun 4948	. . . 4 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)
3	2	imbi1i 349	. . 3 ⊢ ((𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → 𝑦 ∈ 𝐶) ↔ (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
4	3	albii 1820	. 2 ⊢ (∀𝑦(𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
5		df-ss 3916	. . . 4 ⊢ (𝐵 ⊆ 𝐶 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
6	5	ralbii 3080	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
7		ralcom4 3260	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑦∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
8		r19.23v 3161	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
9	8	albii 1820	. . 3 ⊢ (∀𝑦∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
10	6, 7, 9	3bitrri 298	. 2 ⊢ (∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶)
11	1, 4, 10	3bitri 297	1 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶)

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1539   ∈ wcel 2113  ∀wral 3049  ∃wrex 3058   ⊆ wss 3899  ∪ ciun 4944

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-11 2162  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ral 3050  df-rex 3059  df-v 3440  df-ss 3916  df-iun 4946

This theorem is referenced by:  iunss2  5003  iunssd  5004  reliun  5763  djussxp  5792  fiun  7885  f1iun  7886  frrlem7  8232  onfununi  8271  oawordeulem  8479  oaabslem  8573  oaabs2  8575  omabslem  8576  omabs  8577  marypha2lem1  9336  ttrclselem1  9632  trcl  9635  r1val1  9696  rankuni2b  9763  rankval4  9777  rankbnd  9778  rankbnd2  9779  rankc1  9780  cfslb2n  10176  cfsmolem  10178  hsmexlem2  10335  axdc3lem2  10359  ac6  10388  wuncval2  10656  inar1  10684  tskuni  10692  grur1a  10728  fsuppmapnn0fiublem  13911  fsuppmapnn0fiub  13912  rtrclreclem4  14982  prmreclem4  16845  prmreclem5  16846  prdsval  17373  prdsbas  17375  imasaddfnlem  17447  imasvscafn  17456  imasvscaf  17458  isacs2  17574  mreacs  17579  acsfn  17580  dmcoass  17988  isacs5  18469  dprdspan  19956  dprd2dlem1  19970  dprd2d2  19973  dmdprdsplit2lem  19974  lbsextlem2  21112  lpival  21277  iunocv  21634  tgidm  22922  iunconn  23370  comppfsc  23474  txtube  23582  txcmplem2  23584  xkococnlem  23601  xkoinjcn  23629  alexsubALTlem3  23991  cnextf  24008  imasdsf1olem  24315  metnrmlem3  24804  ovolfiniun  25456  ovoliunlem2  25458  ovoliun  25460  ovoliunnul  25462  volfiniun  25502  voliunlem1  25505  volsup  25511  uniioombllem3a  25539  uniioombllem3  25540  uniioombllem4  25541  ismbf3d  25609  limciun  25849  taylfval  26320  taylf  26322  bdayle  27888  elpwiuncl  32551  disjunsn  32618  gsumpart  33095  esum2d  34199  omssubadd  34406  eulerpartlemgh  34484  eulerpartlemgs2  34486  bnj226  34839  bnj517  34990  bnj1118  35089  bnj1137  35100  rankval4b  35205  tz9.1regs  35239  cvmlift2lem12  35457  ntruni  36470  neibastop2lem  36503  filnetlem4  36524  mblfinlem2  37798  volsupnfl  37805  cnambfre  37808  sstotbnd2  37914  equivtotbnd  37918  totbndbnd  37929  prdstotbnd  37934  heiborlem1  37951  pclfinN  40099  lcfrlem4  41744  lcfrlem16  41757  lcfr  41784  oaabsb  43478  naddgeoa  43578  naddwordnexlem4  43585  iunrelexp0  43885  iunrelexpmin1  43891  iunrelexpmin2  43895  cotrcltrcl  43908  trclimalb2  43909  cotrclrcl  43925  iunconnlem2  45117  ixpssmapc  45260  ioorrnopnlem  46490  omeiunle  46703  omeiunltfirp  46705  carageniuncl  46709  caratheodorylem1  46712  caratheodorylem2  46713  hoissrrn  46735  ovnlecvr  46744  ovnsubaddlem1  46756  ovnsubadd  46758  hoissrrn2  46764  ovnlecvr2  46796  hspmbl  46815  opnvonmbllem2  46819  vonvolmbllem  46846  vonvolmbl2  46849  vonvol2  46850  iunhoiioolem  46861  iunhoiioo  46862  iuneq0  49006  iuneqconst2  49010  imassc  49340