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

Theorem ssiun2 4218
Description: Identity law for subset of an indexed union. (Contributed by NM, 12-Oct-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
Assertion
Ref Expression
ssiun2  |-  ( x  e.  A  ->  B  C_ 
U_ x  e.  A  B )

Proof of Theorem ssiun2
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 rspe 2782 . . . 4  |-  ( ( x  e.  A  /\  y  e.  B )  ->  E. x  e.  A  y  e.  B )
21ex 434 . . 3  |-  ( x  e.  A  ->  (
y  e.  B  ->  E. x  e.  A  y  e.  B )
)
3 eliun 4180 . . 3  |-  ( y  e.  U_ x  e.  A  B  <->  E. x  e.  A  y  e.  B )
42, 3syl6ibr 227 . 2  |-  ( x  e.  A  ->  (
y  e.  B  -> 
y  e.  U_ x  e.  A  B )
)
54ssrdv 3367 1  |-  ( x  e.  A  ->  B  C_ 
U_ x  e.  A  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756   E.wrex 2721    C_ wss 3333   U_ciun 4176
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 2573  df-ral 2725  df-rex 2726  df-v 2979  df-in 3340  df-ss 3347  df-iun 4178
This theorem is referenced by:  ssiun2s  4219  disjxiun  4294  triun  4403  ixpf  7290  ixpiunwdom  7811  r1sdom  7986  r1val1  7998  rankuni2b  8065  rankval4  8079  cplem1  8101  domtriomlem  8616  ac6num  8653  iunfo  8708  iundom2g  8709  pwfseqlem3  8832  inar1  8947  tskuni  8955  iunconlem  19036  ptclsg  19193  ovoliunlem1  20990  limciun  21374  ssiun2sf  25915  trpredrec  27707  bnj906  31928  bnj999  31955  bnj1014  31958  bnj1408  32032
  Copyright terms: Public domain W3C validator