Theorem iunss 4561

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	|- ( U_ x e. A B C_ C <-> A. x e. A B C_ C )

Distinct variable group:   x, C

Allowed substitution hints:   A( x)   B( x)

Proof of Theorem iunss

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-iun 4522	. . 3 |- U_ x e. A B = { y | E. x e. A y e. B }
2	1	sseq1i 3629	. 2 |- ( U_ x e. A B C_ C <-> { y | E. x e. A y e. B } C_ C )
3		abss 3671	. 2 |- ( { y | E. x e. A y e. B } C_ C <-> A. y ( E. x e. A y e. B -> y e. C ) )
4		dfss2 3591	. . . 4 |- ( B C_ C <-> A. y ( y e. B -> y e. C ) )
5	4	ralbii 2980	. . 3 |- ( A. x e. A B C_ C <-> A. x e. A A. y ( y e. B -> y e. C ) )
6		ralcom4 3224	. . 3 |- ( A. x e. A A. y ( y e. B -> y e. C ) <-> A. y A. x e. A ( y e. B -> y e. C ) )
7		r19.23v 3023	. . . 4 |- ( A. x e. A ( y e. B -> y e. C ) <-> ( E. x e. A y e. B -> y e. C ) )
8	7	albii 1747	. . 3 |- ( A. y A. x e. A ( y e. B -> y e. C ) <-> A. y ( E. x e. A y e. B -> y e. C ) )
9	5, 6, 8	3bitrri 287	. 2 |- ( A. y ( E. x e. A y e. B -> y e. C ) <-> A. x e. A B C_ C )
10	2, 3, 9	3bitri 286	1 |- ( U_ x e. A B C_ C <-> A. x e. A B C_ C )

Syntax hints:   -> wi 4   <-> wb 196   A.wal 1481   e. wcel 1990   {cab 2608   A.wral 2912   E.wrex 2913   C_ wss 3574   U_ciun 4520

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-v 3202  df-in 3581  df-ss 3588  df-iun 4522

This theorem is referenced by:  iunss2  4565  djussxp  5267  fun11iun  7126  wfrdmss  7421  onfununi  7438  oawordeulem  7634  oaabslem  7723  oaabs2  7725  omabslem  7726  omabs  7727  marypha2lem1  8341  trcl  8604  r1val1  8649  rankuni2b  8716  rankval4  8730  rankbnd  8731  rankbnd2  8732  rankc1  8733  cfslb2n  9090  cfsmolem  9092  hsmexlem2  9249  axdc3lem2  9273  ac6  9302  wuncval2  9569  inar1  9597  tskuni  9605  grur1a  9641  fsuppmapnn0fiublem  12789  fsuppmapnn0fiub  12790  fsuppmapnn0fiubOLD  12791  wrdexg  13315  rtrclreclem4  13801  prmreclem4  15623  prmreclem5  15624  prdsval  16115  prdsbas  16117  imasaddfnlem  16188  imasaddflem  16190  imasvscafn  16197  imasvscaf  16199  isacs2  16314  mreacs  16319  acsfn  16320  dmcoass  16716  isacs5  17172  dprdspan  18426  dprd2dlem1  18440  dprd2d2  18443  dmdprdsplit2lem  18444  lbsextlem2  19159  lpival  19245  iunocv  20025  tgidm  20784  iunconn  21231  comppfsc  21335  txtube  21443  txcmplem2  21445  xkococnlem  21462  xkoinjcn  21490  alexsubALTlem3  21853  cnextf  21870  imasdsf1olem  22178  metnrmlem3  22664  ovolfiniun  23269  ovoliunlem2  23271  ovoliun  23273  ovoliunnul  23275  volfiniun  23315  voliunlem1  23318  volsup  23324  uniioombllem3a  23352  uniioombllem3  23353  uniioombllem4  23354  ismbf3d  23421  limciun  23658  taylfval  24113  taylf  24115  elpwiuncl  29359  disjunsn  29407  esum2d  30155  omssubadd  30362  eulerpartlemgh  30440  eulerpartlemgs2  30442  bnj226  30802  bnj517  30955  bnj1118  31052  bnj1137  31063  cvmlift2lem12  31296  trpredlem1  31727  trpredss  31729  trpredmintr  31731  dftrpred3g  31733  frrlem5d  31787  frrlem7  31790  ntruni  32322  neibastop2lem  32355  filnetlem4  32376  mblfinlem2  33447  volsupnfl  33454  cnambfre  33458  sstotbnd2  33573  equivtotbnd  33577  totbndbnd  33588  prdstotbnd  33593  heiborlem1  33610  pclfinN  35186  lcfrlem4  36834  lcfrlem16  36847  lcfr  36874  iunrelexp0  37994  iunrelexpmin1  38000  iunrelexpmin2  38004  cotrcltrcl  38017  trclimalb2  38018  cotrclrcl  38034  iunconnlem2  39171  ixpssmapc  39243  iunssd  39271  ioorrnopnlem  40524  omeiunle  40731  omeiunltfirp  40733  carageniuncl  40737  caratheodorylem1  40740  caratheodorylem2  40741  hoissrrn  40763  ovnlecvr  40772  ovnsubaddlem1  40784  ovnsubadd  40786  hoissrrn2  40792  ovnlecvr2  40824  hspmbl  40843  opnvonmbllem2  40847  vonvolmbllem  40874  vonvolmbl2  40877  vonvol2  40878  iunhoiioolem  40889  iunhoiioo  40890