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

Theorem ssint 3879
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  |-  ( A 
C_  |^| B  <->  A. x  e.  B  A  C_  x
)
Distinct variable groups:    x, A    x, B

Proof of Theorem ssint
StepHypRef Expression
1 dfss3 3171 . 2  |-  ( A 
C_  |^| B  <->  A. y  e.  A  y  e.  |^| B )
2 vex 2792 . . . 4  |-  y  e. 
_V
32elint2 3870 . . 3  |-  ( y  e.  |^| B  <->  A. x  e.  B  y  e.  x )
43ralbii 2568 . 2  |-  ( A. y  e.  A  y  e.  |^| B  <->  A. y  e.  A  A. x  e.  B  y  e.  x )
5 ralcom 2701 . . 3  |-  ( A. y  e.  A  A. x  e.  B  y  e.  x  <->  A. x  e.  B  A. y  e.  A  y  e.  x )
6 dfss3 3171 . . . 4  |-  ( A 
C_  x  <->  A. y  e.  A  y  e.  x )
76ralbii 2568 . . 3  |-  ( A. x  e.  B  A  C_  x  <->  A. x  e.  B  A. y  e.  A  y  e.  x )
85, 7bitr4i 245 . 2  |-  ( A. y  e.  A  A. x  e.  B  y  e.  x  <->  A. x  e.  B  A  C_  x )
91, 4, 83bitri 264 1  |-  ( A 
C_  |^| B  <->  A. x  e.  B  A  C_  x
)
Colors of variables: wff set class
Syntax hints:    <-> wb 178    e. wcel 1688   A.wral 2544    C_ wss 3153   |^|cint 3863
This theorem is referenced by:  ssintab  3880  ssintub  3881  iinpw  3991  trint  4129  oneqmini  4442  fint  5385  sorpssint  6248  iscard2  7604  coftr  7894  isf32lem2  7975  inttsk  8391  isacs1i  13553  mrelatglb  14281  fbfinnfr  17530  fclscmp  17719  dfrtrcl2  23449  fneint  25676  topmeet  25712  igenval2  26090  ismrcd1  26172
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1538  ax-5 1549  ax-17 1608  ax-9 1641  ax-8 1648  ax-6 1707  ax-7 1712  ax-11 1719  ax-12 1869  ax-ext 2265
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1534  df-nf 1537  df-sb 1636  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-ral 2549  df-v 2791  df-in 3160  df-ss 3167  df-int 3864
  Copyright terms: Public domain W3C validator