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

Theorem ss2iun 4287
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 3436 . . . . 5  |-  ( B 
C_  C  ->  (
y  e.  B  -> 
y  e.  C ) )
21ralimi 2797 . . . 4  |-  ( A. x  e.  A  B  C_  C  ->  A. x  e.  A  ( y  e.  B  ->  y  e.  C ) )
3 rexim 2869 . . . 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 17 . . 3  |-  ( A. x  e.  A  B  C_  C  ->  ( E. x  e.  A  y  e.  B  ->  E. x  e.  A  y  e.  C ) )
5 eliun 4276 . . 3  |-  ( y  e.  U_ x  e.  A  B  <->  E. x  e.  A  y  e.  B )
6 eliun 4276 . . 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 3448 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 1842   A.wral 2754   E.wrex 2755    C_ wss 3414   U_ciun 4271
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ral 2759  df-rex 2760  df-v 3061  df-in 3421  df-ss 3428  df-iun 4273
This theorem is referenced by:  iuneq2  4288  oawordri  7236  omwordri  7258  oewordri  7278  oeworde  7279  r1val1  8236  cfslb2n  8680  imasaddvallem  15143  dprdss  17396  tgcmp  20194  txcmplem1  20434  txcmplem2  20435  xkococnlem  20452  alexsubALT  20843  ptcmplem3  20846  metnrmlem2  21656  uniiccvol  22281  dvfval  22593  bnj1145  29376  bnj1136  29380  filnetlem3  30608  sstotbnd2  31552  equivtotbnd  31556  trclrelexplem  35690  corcltrcl  35718  cotrclrcl  35721
  Copyright terms: Public domain W3C validator