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

Theorem ssiun2s 4359
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 2605 . 2  |-  F/_ x C
2 nfcv 2605 . . 3  |-  F/_ x D
3 nfiu1 4345 . . 3  |-  F/_ x U_ x  e.  A  B
42, 3nfss 3482 . 2  |-  F/ x  D  C_  U_ x  e.  A  B
5 ssiun2s.1 . . 3  |-  ( x  =  C  ->  B  =  D )
65sseq1d 3516 . 2  |-  ( x  =  C  ->  ( B  C_  U_ x  e.  A  B  <->  D  C_  U_ x  e.  A  B )
)
7 ssiun2 4358 . 2  |-  ( x  e.  A  ->  B  C_ 
U_ x  e.  A  B )
81, 4, 6, 7vtoclgaf 3158 1  |-  ( C  e.  A  ->  D  C_ 
U_ x  e.  A  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1383    e. wcel 1804    C_ wss 3461   U_ciun 4315
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ral 2798  df-rex 2799  df-v 3097  df-in 3468  df-ss 3475  df-iun 4317
This theorem is referenced by:  onfununi  7014  oaordi  7197  omordi  7217  dffi3  7893  alephordi  8458  domtriomlem  8825  pwxpndom2  9046  wunex2  9119  imasaddvallem  14908  imasvscaval  14917  iundisj2  21937  voliunlem1  21938  volsup  21944  iundisj2fi  27580  cvmliftlem10  28717  cvmliftlem13  28719  sstotbnd2  30246  bnj906  33856  bnj1137  33919  bnj1408  33960  mapdrvallem3  37248
  Copyright terms: Public domain W3C validator