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

Theorem ssiun2 4373
 Description: Identity law for subset of an indexed union. (Contributed by NM, 12-Oct-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
Assertion
Ref Expression
ssiun2

Proof of Theorem ssiun2
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 rspe 2915 . . . 4
21ex 434 . . 3
3 eliun 4335 . . 3
42, 3syl6ibr 227 . 2
54ssrdv 3509 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  e.wcel 1818  E.wrex 2808  C_wss 3475  U_ciun 4330 This theorem is referenced by:  ssiun2s  4374  disjxiun  4449  triun  4558  ixpf  7511  ixpiunwdom  8038  r1sdom  8213  r1val1  8225  rankuni2b  8292  rankval4  8306  cplem1  8328  domtriomlem  8843  ac6num  8880  iunfo  8935  iundom2g  8936  pwfseqlem3  9059  inar1  9174  tskuni  9182  iunconlem  19928  ptclsg  20116  ovoliunlem1  21913  limciun  22298  ssiun2sf  27427  trpredrec  29321  bnj906  33988  bnj999  34015  bnj1014  34018  bnj1408  34092 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-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