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

Theorem ssiun2s 4207
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 2573 . 2  |-  F/_ x C
2 nfcv 2573 . . 3  |-  F/_ x D
3 nfiu1 4193 . . 3  |-  F/_ x U_ x  e.  A  B
42, 3nfss 3342 . 2  |-  F/ x  D  C_  U_ x  e.  A  B
5 ssiun2s.1 . . 3  |-  ( x  =  C  ->  B  =  D )
65sseq1d 3376 . 2  |-  ( x  =  C  ->  ( B  C_  U_ x  e.  A  B  <->  D  C_  U_ x  e.  A  B )
)
7 ssiun2 4206 . 2  |-  ( x  e.  A  ->  B  C_ 
U_ x  e.  A  B )
81, 4, 6, 7vtoclgaf 3028 1  |-  ( C  e.  A  ->  D  C_ 
U_ x  e.  A  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369    e. wcel 1756    C_ wss 3321   U_ciun 4164
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 2418
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 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ral 2714  df-rex 2715  df-v 2968  df-in 3328  df-ss 3335  df-iun 4166
This theorem is referenced by:  onfununi  6794  oaordi  6977  omordi  6997  dffi3  7673  alephordi  8236  domtriomlem  8603  pwxpndom2  8824  wunex2  8897  imasaddvallem  14459  imasvscaval  14468  iundisj2  20999  voliunlem1  21000  volsup  21006  iundisj2fi  26026  cvmliftlem10  27131  cvmliftlem13  27133  sstotbnd2  28616  bnj906  31780  bnj1137  31843  bnj1408  31884  mapdrvallem3  35042
  Copyright terms: Public domain W3C validator