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

Theorem ss2iun 4186
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 3350 . . . . 5  |-  ( B 
C_  C  ->  (
y  e.  B  -> 
y  e.  C ) )
21ralimi 2791 . . . 4  |-  ( A. x  e.  A  B  C_  C  ->  A. x  e.  A  ( y  e.  B  ->  y  e.  C ) )
3 rexim 2820 . . . 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 4175 . . 3  |-  ( y  e.  U_ x  e.  A  B  <->  E. x  e.  A  y  e.  B )
6 eliun 4175 . . 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 3362 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 1756   A.wral 2715   E.wrex 2716    C_ wss 3328   U_ciun 4171
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ral 2720  df-rex 2721  df-v 2974  df-in 3335  df-ss 3342  df-iun 4173
This theorem is referenced by:  iuneq2  4187  oawordri  6989  omwordri  7011  oewordri  7031  oeworde  7032  r1val1  7993  cfslb2n  8437  imasaddvallem  14467  dprdss  16526  tgcmp  19004  txcmplem1  19214  txcmplem2  19215  xkococnlem  19232  alexsubALT  19623  ptcmplem3  19626  metnrmlem2  20436  uniiccvol  21060  dvfval  21372  filnetlem3  28601  sstotbnd2  28673  equivtotbnd  28677  bnj1145  31984  bnj1136  31988
  Copyright terms: Public domain W3C validator