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

Theorem ss2iun 4341
Description: Subclass theorem for indexed union. (Contributed by NM, 26-Nov-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
Assertion
Ref Expression
ss2iun  |-  ( A. x  e.  A  B  C_  C  ->  U_ x  e.  A  B  C_  U_ x  e.  A  C )

Proof of Theorem ss2iun
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 ssel 3498 . . . . 5  |-  ( B 
C_  C  ->  (
y  e.  B  -> 
y  e.  C ) )
21ralimi 2857 . . . 4  |-  ( A. x  e.  A  B  C_  C  ->  A. x  e.  A  ( y  e.  B  ->  y  e.  C ) )
3 rexim 2929 . . . 4  |-  ( A. x  e.  A  (
y  e.  B  -> 
y  e.  C )  ->  ( E. x  e.  A  y  e.  B  ->  E. x  e.  A  y  e.  C )
)
42, 3syl 16 . . 3  |-  ( A. x  e.  A  B  C_  C  ->  ( E. x  e.  A  y  e.  B  ->  E. x  e.  A  y  e.  C ) )
5 eliun 4330 . . 3  |-  ( y  e.  U_ x  e.  A  B  <->  E. x  e.  A  y  e.  B )
6 eliun 4330 . . 3  |-  ( y  e.  U_ x  e.  A  C  <->  E. x  e.  A  y  e.  C )
74, 5, 63imtr4g 270 . 2  |-  ( A. x  e.  A  B  C_  C  ->  ( y  e.  U_ x  e.  A  B  ->  y  e.  U_ x  e.  A  C
) )
87ssrdv 3510 1  |-  ( A. x  e.  A  B  C_  C  ->  U_ x  e.  A  B  C_  U_ x  e.  A  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1767   A.wral 2814   E.wrex 2815    C_ wss 3476   U_ciun 4325
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ral 2819  df-rex 2820  df-v 3115  df-in 3483  df-ss 3490  df-iun 4327
This theorem is referenced by:  iuneq2  4342  oawordri  7199  omwordri  7221  oewordri  7241  oeworde  7242  r1val1  8204  cfslb2n  8648  imasaddvallem  14784  dprdss  16878  tgcmp  19695  txcmplem1  19905  txcmplem2  19906  xkococnlem  19923  alexsubALT  20314  ptcmplem3  20317  metnrmlem2  21127  uniiccvol  21752  dvfval  22064  filnetlem3  29829  sstotbnd2  29901  equivtotbnd  29905  bnj1145  33146  bnj1136  33150
  Copyright terms: Public domain W3C validator