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

Theorem ssiun2 3945
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 2604 . . . 4  |-  ( ( x  e.  A  /\  y  e.  B )  ->  E. x  e.  A  y  e.  B )
21ex 423 . . 3  |-  ( x  e.  A  ->  (
y  e.  B  ->  E. x  e.  A  y  e.  B )
)
3 eliun 3909 . . 3  |-  ( y  e.  U_ x  e.  A  B  <->  E. x  e.  A  y  e.  B )
42, 3syl6ibr 218 . 2  |-  ( x  e.  A  ->  (
y  e.  B  -> 
y  e.  U_ x  e.  A  B )
)
54ssrdv 3185 1  |-  ( x  e.  A  ->  B  C_ 
U_ x  e.  A  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1684   E.wrex 2544    C_ wss 3152   U_ciun 3905
This theorem is referenced by:  ssiun2s  3946  disjxiun  4020  triun  4126  ixpf  6838  ixpiunwdom  7305  r1sdom  7446  r1val1  7458  rankuni2b  7525  rankval4  7539  cplem1  7559  domtriomlem  8068  ac6num  8106  iunfo  8161  iundom2g  8162  pwfseqlem3  8282  inar1  8397  tskuni  8405  iunconlem  17153  ptclsg  17309  ovoliunlem1  18861  limciun  19244  ssiun2sf  23157  trpredrec  24241  bnj906  28962  bnj999  28989  bnj1014  28992  bnj1408  29066
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