Theorem iunss 4371

Description: Subset theorem for an indexed union. (Contributed by NM, 13-Sep-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)

Assertion

Ref	Expression
iunss

Distinct variable group:   ,

Proof of Theorem iunss

Dummy variable is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-iun 4332	. . 3
2	1	sseq1i 3527	. 2
3		abss 3568	. 2
4		dfss2 3492	. . . 4
5	4	ralbii 2888	. . 3
6		ralcom4 3128	. . 3
7		r19.23v 2937	. . . 4
8	7	albii 1640	. . 3
9	5, 6, 8	3bitrri 272	. 2
10	2, 3, 9	3bitri 271	1

Syntax hints:  ->wi 4  <->wb 184  A.wal 1393  e.wcel 1818  {cab 2442  A.wral 2807  E.wrex 2808  C_wss 3475  U_ciun 4330

This theorem is referenced by:  iunss2  4375  djussxp  5153  fun11iun  6760  onfununi  7031  oawordeulem  7222  oaabslem  7311  oaabs2  7313  omabslem  7314  omabs  7315  marypha2lem1  7915  trcl  8180  r1val1  8225  rankuni2b  8292  rankval4  8306  rankbnd  8307  rankbnd2  8308  rankc1  8309  cfslb2n  8669  cfsmolem  8671  hsmexlem2  8828  axdc3lem2  8852  ac6  8881  wuncval2  9146  inar1  9174  tskuni  9182  grur1a  9218  fsuppmapnn0fiublem  12096  fsuppmapnn0fiub  12097  wrdexg  12557  prmreclem4  14437  prmreclem5  14438  prdsval  14852  prdsbas  14854  imasaddfnlem  14925  imasaddflem  14927  imasvscafn  14934  imasvscaf  14936  isacs2  15050  mreacs  15055  acsfn  15056  dmcoass  15393  isacs5  15802  dprdspan  17074  dprd2dlem1  17090  dprd2d2  17093  dmdprdsplit2lem  17094  lbsextlem2  17805  lpival  17893  iunocv  18712  tgidm  19482  iuncon  19929  comppfsc  20033  txtube  20141  txcmplem2  20143  xkococnlem  20160  xkoinjcn  20188  alexsubALTlem3  20549  cnextf  20566  imasdsf1olem  20876  metnrmlem3  21365  ovolfiniun  21912  ovoliunlem2  21914  ovoliun  21916  ovoliunnul  21918  volfiniun  21957  voliunlem1  21960  volsup  21966  uniioombllem3a  21993  uniioombllem3  21994  uniioombllem4  21995  ismbf3d  22061  limciun  22298  taylfval  22754  taylf  22756  disjunsn  27453  eulerpartlemgh  28317  eulerpartlemgs2  28319  cvmlift2lem12  28759  rtrclreclem.min  29070  trpredlem1  29310  trpredss  29312  trpredmintr  29314  dftrpred3g  29316  wfrlem7  29349  frrlem5d  29394  frrlem7  29397  nofulllem5  29466  mblfinlem2  30052  volsupnfl  30059  cnambfre  30063  ntruni  30145  neibastop2lem  30178  filnetlem4  30199  sstotbnd2  30270  equivtotbnd  30274  totbndbnd  30285  prdstotbnd  30290  heiborlem1  30307  iunconlem2  33735  bnj226  33789  bnj517  33943  bnj1118  34040  bnj1137  34051  pclfinN  35624  lcfrlem4  37272  lcfrlem16  37285  lcfr  37312

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812  df-rex 2813  df-v 3111  df-in 3482  df-ss 3489  df-iun 4332