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

Theorem ss2in 3691
Description: Intersection of subclasses. (Contributed by NM, 5-May-2000.)
Assertion
Ref Expression
ss2in

Proof of Theorem ss2in
StepHypRef Expression
1 ssrin 3689 . 2
2 sslin 3690 . 2
31, 2sylan9ss 3483 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  i^icin 3441  C_wss 3442
This theorem is referenced by:  disjxiun  4406  undom  7533  strlemor1  14424  strleun  14427  dprdss  16701  dprd2da  16716  ablfac1b  16746  tgcl  18973  innei  19128  hausnei2  19356  bwth  19412  fbssfi  19809  fbunfip  19841  fgcl  19850  blin2  20403  vdgrun  24040  vdgrfiun  24041  5oai  25533  mayetes3i  25602  mdsl0  26183  ismblfin  28892  neibastop1  29040  heibor1lem  29168  icccncfext  30455  pl42lem2N  34475  pl42lem3N  34476
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3083  df-in 3449  df-ss 3456
  Copyright terms: Public domain W3C validator