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

Theorem ssiun2s 3946
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 2419 . 2  |-  F/_ x C
2 nfcv 2419 . . 3  |-  F/_ x D
3 nfiu1 3933 . . 3  |-  F/_ x U_ x  e.  A  B
42, 3nfss 3173 . 2  |-  F/ x  D  C_  U_ x  e.  A  B
5 ssiun2s.1 . . 3  |-  ( x  =  C  ->  B  =  D )
65sseq1d 3205 . 2  |-  ( x  =  C  ->  ( B  C_  U_ x  e.  A  B  <->  D  C_  U_ x  e.  A  B )
)
7 ssiun2 3945 . 2  |-  ( x  e.  A  ->  B  C_ 
U_ x  e.  A  B )
81, 4, 6, 7vtoclgaf 2848 1  |-  ( C  e.  A  ->  D  C_ 
U_ x  e.  A  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    e. wcel 1684    C_ wss 3152   U_ciun 3905
This theorem is referenced by:  onfununi  6358  oaordi  6544  omordi  6564  dffi3  7184  alephordi  7701  domtriomlem  8068  pwxpndom2  8287  wunex2  8360  imasaddvallem  13431  imasvscaval  13440  iundisj2  18906  voliunlem1  18907  volsup  18913  iundisj2fi  23364  cvmliftlem10  23825  cvmliftlem13  23827  sstotbnd2  26498  bnj906  28962  bnj1137  29025  bnj1408  29066  mapdrvallem3  31836
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