MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  iunss Unicode version

Theorem iunss 4100
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.
StepHypRef Expression
1 df-iun 4063 . . 3  |-  U_ x  e.  A  B  =  { y  |  E. x  e.  A  y  e.  B }
21sseq1i 3340 . 2  |-  ( U_ x  e.  A  B  C_  C  <->  { y  |  E. x  e.  A  y  e.  B }  C_  C
)
3 abss 3380 . 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 3305 . . . 4  |-  ( B 
C_  C  <->  A. y
( y  e.  B  ->  y  e.  C ) )
54ralbii 2698 . . 3  |-  ( A. x  e.  A  B  C_  C  <->  A. x  e.  A  A. y ( y  e.  B  ->  y  e.  C ) )
6 ralcom4 2942 . . 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 2790 . . . 4  |-  ( A. x  e.  A  (
y  e.  B  -> 
y  e.  C )  <-> 
( E. x  e.  A  y  e.  B  ->  y  e.  C ) )
87albii 1572 . . 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
) )
95, 6, 83bitrri 264 . 2  |-  ( A. y ( E. x  e.  A  y  e.  B  ->  y  e.  C
)  <->  A. x  e.  A  B  C_  C )
102, 3, 93bitri 263 1  |-  ( U_ x  e.  A  B  C_  C  <->  A. x  e.  A  B  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177   A.wal 1546    e. wcel 1721   {cab 2398   A.wral 2674   E.wrex 2675    C_ wss 3288   U_ciun 4061
This theorem is referenced by:  iunss2  4104  djussxp  4985  fun11iun  5662  onfununi  6570  oawordeulem  6764  oaabslem  6853  oaabs2  6855  omabslem  6856  omabs  6857  marypha2lem1  7406  trcl  7628  r1val1  7676  rankuni2b  7743  rankval4  7757  rankbnd  7758  rankbnd2  7759  rankc1  7760  cfslb2n  8112  cfsmolem  8114  hsmexlem2  8271  axdc3lem2  8295  ac6  8324  wuncval2  8586  inar1  8614  tskuni  8622  grur1a  8658  wrdexg  11702  prmreclem4  13250  prmreclem5  13251  prdsval  13641  prdsbas  13643  imasaddfnlem  13716  imasaddflem  13718  imasvscafn  13725  imasvscaf  13727  isacs2  13841  mreacs  13846  acsfn  13847  dmcoass  14184  isacs5  14561  dprdspan  15548  dprd2dlem1  15562  dprd2d2  15565  dmdprdsplit2lem  15566  lbsextlem2  16194  lpival  16279  iunocv  16871  tgidm  17008  iuncon  17452  txtube  17633  txcmplem2  17635  xkococnlem  17652  xkoinjcn  17680  alexsubALTlem3  18041  cnextf  18058  imasdsf1olem  18364  metnrmlem3  18852  ovolfiniun  19358  ovoliunlem2  19360  ovoliun  19362  ovoliunnul  19364  volfiniun  19402  voliunlem1  19405  volsup  19411  uniioombllem3a  19437  uniioombllem3  19438  uniioombllem4  19439  ismbf3d  19507  limciun  19742  taylfval  20236  taylf  20238  cvmlift2lem12  24962  rtrclreclem.min  25108  trpredlem1  25452  trpredss  25454  trpredmintr  25456  dftrpred3g  25458  wfrlem7  25484  frrlem5d  25510  frrlem7  25513  nofulllem5  25582  mblfinlem  26151  volsupnfl  26158  cnambfre  26162  ntruni  26228  comppfsc  26285  neibastop2lem  26287  filnetlem4  26308  sstotbnd2  26381  equivtotbnd  26385  totbndbnd  26396  prdstotbnd  26401  heiborlem1  26418  iunconlem2  28766  bnj226  28819  bnj517  28974  bnj1118  29071  bnj1137  29082  pclfinN  30394  lcfrlem4  32040  lcfrlem16  32053  lcfr  32080
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-ral 2679  df-rex 2680  df-v 2926  df-in 3295  df-ss 3302  df-iun 4063
  Copyright terms: Public domain W3C validator