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

Theorem ssint 3878
 Description: Subclass of a class intersection. Theorem 5.11(viii) of [Monk1] p. 52 and its converse. (Contributed by NM, 14-Oct-1999.)
Assertion
Ref Expression
ssint
Distinct variable groups:   ,   ,

Proof of Theorem ssint
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 dfss3 3170 . 2
2 vex 2791 . . . 4
32elint2 3869 . . 3
43ralbii 2567 . 2
5 ralcom 2700 . . 3
6 dfss3 3170 . . . 4
76ralbii 2567 . . 3
85, 7bitr4i 243 . 2
91, 4, 83bitri 262 1
 Colors of variables: wff set class Syntax hints:   wb 176   wcel 1684  wral 2543   wss 3152  cint 3862 This theorem is referenced by:  ssintab  3879  ssintub  3880  iinpw  3990  trint  4128  oneqmini  4443  fint  5420  sorpssint  6287  iscard2  7609  coftr  7899  isf32lem2  7980  inttsk  8396  isacs1i  13559  mrelatglb  14287  fbfinnfr  17536  fclscmp  17725  dfrtrcl2  24045  fneint  26277  topmeet  26313  igenval2  26691  ismrcd1  26773 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548  df-v 2790  df-in 3159  df-ss 3166  df-int 3863
 Copyright terms: Public domain W3C validator