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

Theorem intss 4303
 Description: Intersection of subclasses. (Contributed by NM, 14-Oct-1999.)
Assertion
Ref Expression
intss

Proof of Theorem intss
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 imim1 76 . . . . 5
21al2imi 1616 . . . 4
3 vex 3116 . . . . 5
43elint 4288 . . . 4
53elint 4288 . . . 4
62, 4, 53imtr4g 270 . . 3
76alrimiv 1695 . 2
8 dfss2 3493 . 2
9 dfss2 3493 . 2
107, 8, 93imtr4i 266 1
 Colors of variables: wff setvar class Syntax hints:   wi 4  wal 1377   wcel 1767   wss 3476  cint 4282 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445 This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-in 3483  df-ss 3490  df-int 4283 This theorem is referenced by:  uniintsn  4319  intabs  4608  fiss  7880  tc2  8169  tcss  8171  tcel  8172  rankval4  8281  cfub  8625  cflm  8626  cflecard  8629  fin23lem26  8701  mrcss  14864  lspss  17410  lbsextlem3  17586  aspss  17749  clsss  19318  1stcfb  19709  ufinffr  20162  spanss  25939  pclssN  34690  dochspss  36175
 Copyright terms: Public domain W3C validator