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

Theorem ssiun2s 4312
Description: Subset relationship for an indexed union. (Contributed by NM, 26-Oct-2003.)
Hypothesis
Ref Expression
ssiun2s.1  |-  ( x  =  C  ->  B  =  D )
Assertion
Ref Expression
ssiun2s  |-  ( C  e.  A  ->  D  C_ 
U_ x  e.  A  B )
Distinct variable groups:    x, A    x, C    x, D
Allowed substitution hint:    B( x)

Proof of Theorem ssiun2s
StepHypRef Expression
1 nfcv 2613 . 2  |-  F/_ x C
2 nfcv 2613 . . 3  |-  F/_ x D
3 nfiu1 4298 . . 3  |-  F/_ x U_ x  e.  A  B
42, 3nfss 3447 . 2  |-  F/ x  D  C_  U_ x  e.  A  B
5 ssiun2s.1 . . 3  |-  ( x  =  C  ->  B  =  D )
65sseq1d 3481 . 2  |-  ( x  =  C  ->  ( B  C_  U_ x  e.  A  B  <->  D  C_  U_ x  e.  A  B )
)
7 ssiun2 4311 . 2  |-  ( x  e.  A  ->  B  C_ 
U_ x  e.  A  B )
81, 4, 6, 7vtoclgaf 3131 1  |-  ( C  e.  A  ->  D  C_ 
U_ x  e.  A  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1370    e. wcel 1758    C_ wss 3426   U_ciun 4269
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ral 2800  df-rex 2801  df-v 3070  df-in 3433  df-ss 3440  df-iun 4271
This theorem is referenced by:  onfununi  6902  oaordi  7085  omordi  7105  dffi3  7782  alephordi  8345  domtriomlem  8712  pwxpndom2  8933  wunex2  9006  imasaddvallem  14569  imasvscaval  14578  iundisj2  21146  voliunlem1  21147  volsup  21153  iundisj2fi  26215  cvmliftlem10  27317  cvmliftlem13  27319  sstotbnd2  28811  bnj906  32223  bnj1137  32286  bnj1408  32327  mapdrvallem3  35597
  Copyright terms: Public domain W3C validator