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

Theorem ssiun2s 4374
 Description: Subset relationship for an indexed union. (Contributed by NM, 26-Oct-2003.)
Hypothesis
Ref Expression
ssiun2s.1
Assertion
Ref Expression
ssiun2s
Distinct variable groups:   ,   ,   ,

Proof of Theorem ssiun2s
StepHypRef Expression
1 nfcv 2619 . 2
2 nfcv 2619 . . 3
3 nfiu1 4360 . . 3
42, 3nfss 3496 . 2
5 ssiun2s.1 . . 3
65sseq1d 3530 . 2
7 ssiun2 4373 . 2
81, 4, 6, 7vtoclgaf 3172 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  =wceq 1395  e.wcel 1818  C_wss 3475  U_ciun 4330 This theorem is referenced by:  onfununi  7031  oaordi  7214  omordi  7234  dffi3  7911  alephordi  8476  domtriomlem  8843  pwxpndom2  9064  wunex2  9137  imasaddvallem  14926  imasvscaval  14935  iundisj2  21959  voliunlem1  21960  volsup  21966  iundisj2fi  27602  cvmliftlem10  28739  cvmliftlem13  28741  sstotbnd2  30270  bnj906  33988  bnj1137  34051  bnj1408  34092  mapdrvallem3  37373 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812  df-rex 2813  df-v 3111  df-in 3482  df-ss 3489  df-iun 4332
 Copyright terms: Public domain W3C validator