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

Theorem iunss 3943
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 3907 . . 3  |-  U_ x  e.  A  B  =  { y  |  E. x  e.  A  y  e.  B }
21sseq1i 3202 . 2  |-  ( U_ x  e.  A  B  C_  C  <->  { y  |  E. x  e.  A  y  e.  B }  C_  C
)
3 abss 3242 . 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 3169 . . . 4  |-  ( B 
C_  C  <->  A. y
( y  e.  B  ->  y  e.  C ) )
54ralbii 2567 . . 3  |-  ( A. x  e.  A  B  C_  C  <->  A. x  e.  A  A. y ( y  e.  B  ->  y  e.  C ) )
6 ralcom4 2806 . . 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 2659 . . . 4  |-  ( A. x  e.  A  (
y  e.  B  -> 
y  e.  C )  <-> 
( E. x  e.  A  y  e.  B  ->  y  e.  C ) )
87albii 1553 . . 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 263 . 2  |-  ( A. y ( E. x  e.  A  y  e.  B  ->  y  e.  C
)  <->  A. x  e.  A  B  C_  C )
102, 3, 93bitri 262 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 176   A.wal 1527    e. wcel 1684   {cab 2269   A.wral 2543   E.wrex 2544    C_ wss 3152   U_ciun 3905
This theorem is referenced by:  iunss2  3947  djussxp  4829  fun11iun  5493  onfununi  6358  oawordeulem  6552  oaabslem  6641  oaabs2  6643  omabslem  6644  omabs  6645  marypha2lem1  7188  trcl  7410  r1val1  7458  rankuni2b  7525  rankval4  7539  rankbnd  7540  rankbnd2  7541  rankc1  7542  cfslb2n  7894  cfsmolem  7896  hsmexlem2  8053  axdc3lem2  8077  ac6  8107  wuncval2  8369  inar1  8397  tskuni  8405  grur1a  8441  wrdexg  11425  prmreclem4  12966  prmreclem5  12967  prdsval  13355  prdsbas  13357  imasaddfnlem  13430  imasaddflem  13432  imasvscafn  13439  imasvscaf  13441  isacs2  13555  mreacs  13560  acsfn  13561  dmcoass  13898  isacs5  14275  dprdspan  15262  dprd2dlem1  15276  dprd2d2  15279  dmdprdsplit2lem  15280  lbsextlem2  15912  lpival  15997  iunocv  16581  tgidm  16718  iuncon  17154  txtube  17334  txcmplem2  17336  xkococnlem  17353  xkoinjcn  17381  alexsubALTlem3  17743  imasdsf1olem  17937  metnrmlem3  18365  ovolfiniun  18860  ovoliunlem2  18862  ovoliun  18864  ovoliunnul  18866  volfiniun  18904  voliunlem1  18907  volsup  18913  uniioombllem3a  18939  uniioombllem3  18940  uniioombllem4  18941  ismbf3d  19009  limciun  19244  taylfval  19738  taylf  19740  cvmlift2lem12  23845  rtrclreclem.min  24044  trpredlem1  24230  trpredss  24232  trpredmintr  24234  dftrpred3g  24236  wfrlem7  24262  frrlem5d  24288  frrlem7  24291  nofulllem5  24360  uncum2  25110  ntruni  26245  comppfsc  26307  neibastop2lem  26309  filnetlem4  26330  sstotbnd2  26498  equivtotbnd  26502  totbndbnd  26513  prdstotbnd  26518  heiborlem1  26535  bnj226  28762  bnj517  28917  bnj1118  29014  bnj1137  29025  pclfinN  30089  lcfrlem4  31735  lcfrlem16  31748  lcfr  31775
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548  df-rex 2549  df-v 2790  df-in 3159  df-ss 3166  df-iun 3907
  Copyright terms: Public domain W3C validator