Theorem iunss 5011

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1568   ∈ wcel 2146  ∀wral 3081  ∃wrex 3091   ⊆ wss 3906  ∪ ciun 4958

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-11 2195  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3082  df-rex 3092  df-v 3459  df-ss 3923  df-iun 4960

This theorem is used by:  iunss2  5016  iunssd  5017  reliun  5805  djussxp  5833  fiun  7946  f1iun  7947  frrlem7  8295  onfununi  8334  oawordeulem  8545  oaabslem  8639  oaabs2  8641  omabslem  8642  omabs  8643  marypha2lem1  9402  ttrclselem1  9701  trcl  9704  r1val1  9765  rankuni2b  9832  rankval4  9846  rankbnd  9847  rankbnd2  9848  rankc1  9849  cfslb2n  10267  cfsmolem  10269  hsmexlem2  10426  axdc3lem2  10450  ac6  10479  wuncval2  10751  inar1  10779  tskuni  10787  grur1a  10823  fsuppmapnn0fiublem  14048  fsuppmapnn0fiub  14049  rtrclreclem4  15126  prmreclem4  17005  prmreclem5  17006  prdsval  17534  prdsbas  17536  imasaddfnlem  17608  imasvscafn  17617  imasvscaf  17619  isacs2  17735  mreacs  17740  acsfn  17741  dmcoass  18149  isacs5  18630  dprdspan  20147  dprd2dlem1  20161  dprd2d2  20164  dmdprdsplit2lem  20165  lbsextlem2  21337  lpival  21546  iunocv  21885  tgidm  23191  iunconn  23639  comppfsc  23744  txtube  23852  txcmplem2  23854  xkococnlem  23871  xkoinjcn  23899  alexsubALTlem3  24261  cnextf  24278  imasdsf1olem  24585  metnrmlem3  25074  ovolfiniun  25715  ovoliunlem2  25717  ovoliun  25719  ovoliunnul  25721  volfiniun  25761  voliunlem1  25764  volsup  25770  uniioombllem3a  25798  uniioombllem3  25799  uniioombllem4  25800  ismbf3d  25868  limciun  26108  taylfval  26577  taylf  26579  bdayle  28164  elpwiuncl  32948  disjunsn  33014  gsumpart  33451  esum2d  34551  omssubadd  34759  eulerpartlemgh  34837  eulerpartlemgs2  34839  bnj226  35192  bnj517  35342  bnj1118  35441  bnj1137  35452  rankval4b  35555  tz9.1regs  35608  cvmlift2lem12  35847  ntruni  36899  neibastop2lem  36932  filnetlem4  36953  ttciunun  37083  mblfinlem2  38370  volsupnfl  38377  cnambfre  38380  sstotbnd2  38487  equivtotbnd  38491  totbndbnd  38502  prdstotbnd  38507  heiborlem1  38524  pclfinN  40736  lcfrlem4  42381  lcfrlem16  42394  lcfr  42421  oaabsb  44098  naddgeoa  44198  naddwordnexlem4  44205  iunrelexp0  44505  iunrelexpmin1  44511  iunrelexpmin2  44515  cotrcltrcl  44528  trclimalb2  44529  cotrclrcl  44545  iunconnlem2  45720  ixpssmapc  45870  ioorrnopnlem  47095  omeiunle  47308  omeiunltfirp  47310  carageniuncl  47314  caratheodorylem1  47317  caratheodorylem2  47318  hoissrrn  47340  ovnlecvr  47349  ovnsubaddlem1  47361  ovnsubadd  47363  hoissrrn2  47369  ovnlecvr2  47401  hspmbl  47420  opnvonmbllem2  47424  vonvolmbllem  47451  vonvolmbl2  47454  vonvol2  47455  iunhoiioolem  47466  iunhoiioo  47467  iuneq0  49673  iuneqconst2  49677  imassc  50007