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

Theorem ssint 4274
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 3460 . 2  |-  ( A 
C_  |^| B  <->  A. y  e.  A  y  e.  |^| B )
2 vex 3090 . . . 4  |-  y  e. 
_V
32elint2 4265 . . 3  |-  ( y  e.  |^| B  <->  A. x  e.  B  y  e.  x )
43ralbii 2863 . 2  |-  ( A. y  e.  A  y  e.  |^| B  <->  A. y  e.  A  A. x  e.  B  y  e.  x )
5 ralcom 2996 . . 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 3460 . . . 4  |-  ( A 
C_  x  <->  A. y  e.  A  y  e.  x )
76ralbii 2863 . . 3  |-  ( A. x  e.  B  A  C_  x  <->  A. x  e.  B  A. y  e.  A  y  e.  x )
85, 7bitr4i 255 . 2  |-  ( A. y  e.  A  A. x  e.  B  y  e.  x  <->  A. x  e.  B  A  C_  x )
91, 4, 83bitri 274 1  |-  ( A 
C_  |^| B  <->  A. x  e.  B  A  C_  x
)
Colors of variables: wff setvar class
Syntax hints:    <-> wb 187    e. wcel 1870   A.wral 2782    C_ wss 3442   |^|cint 4258
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ral 2787  df-v 3089  df-in 3449  df-ss 3456  df-int 4259
This theorem is referenced by:  ssintab  4275  ssintub  4276  iinpw  4394  trint  4535  oneqmini  5493  fint  5779  sorpssint  6595  iscard2  8409  coftr  8701  isf32lem2  8782  inttsk  9198  dfrtrcl2  13104  isacs1i  15514  mrelatglb  16381  fbfinnfr  20787  fclscmp  20976  fneint  30789  topmeet  30805  igenval2  32003  ismrcd1  35249  dftrcl3  35951  dfrtrcl3  35964
  Copyright terms: Public domain W3C validator