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

Theorem ssiun2 4210
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 2775 . . . 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 4172 . . 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 3359 1  |-  ( x  e.  A  ->  B  C_ 
U_ x  e.  A  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1761   E.wrex 2714    C_ wss 3325   U_ciun 4168
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ral 2718  df-rex 2719  df-v 2972  df-in 3332  df-ss 3339  df-iun 4170
This theorem is referenced by:  ssiun2s  4211  disjxiun  4286  triun  4395  ixpf  7281  ixpiunwdom  7802  r1sdom  7977  r1val1  7989  rankuni2b  8056  rankval4  8070  cplem1  8092  domtriomlem  8607  ac6num  8644  iunfo  8699  iundom2g  8700  pwfseqlem3  8823  inar1  8938  tskuni  8946  iunconlem  18990  ptclsg  19147  ovoliunlem1  20944  limciun  21328  ssiun2sf  25845  trpredrec  27631  bnj906  31757  bnj999  31784  bnj1014  31787  bnj1408  31861
  Copyright terms: Public domain W3C validator