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

Theorem ssiun2s 4364
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 2624 . 2  |-  F/_ x C
2 nfcv 2624 . . 3  |-  F/_ x D
3 nfiu1 4350 . . 3  |-  F/_ x U_ x  e.  A  B
42, 3nfss 3492 . 2  |-  F/ x  D  C_  U_ x  e.  A  B
5 ssiun2s.1 . . 3  |-  ( x  =  C  ->  B  =  D )
65sseq1d 3526 . 2  |-  ( x  =  C  ->  ( B  C_  U_ x  e.  A  B  <->  D  C_  U_ x  e.  A  B )
)
7 ssiun2 4363 . 2  |-  ( x  e.  A  ->  B  C_ 
U_ x  e.  A  B )
81, 4, 6, 7vtoclgaf 3171 1  |-  ( C  e.  A  ->  D  C_ 
U_ x  e.  A  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1374    e. wcel 1762    C_ wss 3471   U_ciun 4320
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2612  df-ral 2814  df-rex 2815  df-v 3110  df-in 3478  df-ss 3485  df-iun 4322
This theorem is referenced by:  onfununi  7004  oaordi  7187  omordi  7207  dffi3  7882  alephordi  8446  domtriomlem  8813  pwxpndom2  9034  wunex2  9107  imasaddvallem  14775  imasvscaval  14784  iundisj2  21689  voliunlem1  21690  volsup  21696  iundisj2fi  27258  cvmliftlem10  28367  cvmliftlem13  28369  sstotbnd2  29862  bnj906  32944  bnj1137  33007  bnj1408  33048  mapdrvallem3  36320
  Copyright terms: Public domain W3C validator