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

Proof of Theorem ssint
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 dfss3 3170 . 2  |-  ( A 
C_  |^| B  <->  A. y  e.  A  y  e.  |^| B )
2 vex 2791 . . . 4  |-  y  e. 
_V
32elint2 3869 . . 3  |-  ( y  e.  |^| B  <->  A. x  e.  B  y  e.  x )
43ralbii 2567 . 2  |-  ( A. y  e.  A  y  e.  |^| B  <->  A. y  e.  A  A. x  e.  B  y  e.  x )
5 ralcom 2700 . . 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 3170 . . . 4  |-  ( A 
C_  x  <->  A. y  e.  A  y  e.  x )
76ralbii 2567 . . 3  |-  ( A. x  e.  B  A  C_  x  <->  A. x  e.  B  A. y  e.  A  y  e.  x )
85, 7bitr4i 243 . 2  |-  ( A. y  e.  A  A. x  e.  B  y  e.  x  <->  A. x  e.  B  A  C_  x )
91, 4, 83bitri 262 1  |-  ( A 
C_  |^| B  <->  A. x  e.  B  A  C_  x
)
Colors of variables: wff set class
Syntax hints:    <-> wb 176    e. wcel 1684   A.wral 2543    C_ 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