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

Theorem ssiun2s 4127
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 2571 . 2  |-  F/_ x C
2 nfcv 2571 . . 3  |-  F/_ x D
3 nfiu1 4113 . . 3  |-  F/_ x U_ x  e.  A  B
42, 3nfss 3333 . 2  |-  F/ x  D  C_  U_ x  e.  A  B
5 ssiun2s.1 . . 3  |-  ( x  =  C  ->  B  =  D )
65sseq1d 3367 . 2  |-  ( x  =  C  ->  ( B  C_  U_ x  e.  A  B  <->  D  C_  U_ x  e.  A  B )
)
7 ssiun2 4126 . 2  |-  ( x  e.  A  ->  B  C_ 
U_ x  e.  A  B )
81, 4, 6, 7vtoclgaf 3008 1  |-  ( C  e.  A  ->  D  C_ 
U_ x  e.  A  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652    e. wcel 1725    C_ wss 3312   U_ciun 4085
This theorem is referenced by:  onfununi  6595  oaordi  6781  omordi  6801  dffi3  7428  alephordi  7947  domtriomlem  8314  pwxpndom2  8532  wunex2  8605  imasaddvallem  13746  imasvscaval  13755  iundisj2  19435  voliunlem1  19436  volsup  19442  iundisj2fi  24145  cvmliftlem10  24973  cvmliftlem13  24975  sstotbnd2  26464  bnj906  29228  bnj1137  29291  bnj1408  29332  mapdrvallem3  32371
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ral 2702  df-rex 2703  df-v 2950  df-in 3319  df-ss 3326  df-iun 4087
  Copyright terms: Public domain W3C validator