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

Theorem ssint 4298
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 3494 . 2  |-  ( A 
C_  |^| B  <->  A. y  e.  A  y  e.  |^| B )
2 vex 3116 . . . 4  |-  y  e. 
_V
32elint2 4289 . . 3  |-  ( y  e.  |^| B  <->  A. x  e.  B  y  e.  x )
43ralbii 2895 . 2  |-  ( A. y  e.  A  y  e.  |^| B  <->  A. y  e.  A  A. x  e.  B  y  e.  x )
5 ralcom 3022 . . 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 3494 . . . 4  |-  ( A 
C_  x  <->  A. y  e.  A  y  e.  x )
76ralbii 2895 . . 3  |-  ( A. x  e.  B  A  C_  x  <->  A. x  e.  B  A. y  e.  A  y  e.  x )
85, 7bitr4i 252 . 2  |-  ( A. y  e.  A  A. x  e.  B  y  e.  x  <->  A. x  e.  B  A  C_  x )
91, 4, 83bitri 271 1  |-  ( A 
C_  |^| B  <->  A. x  e.  B  A  C_  x
)
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    e. wcel 1767   A.wral 2814    C_ 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-or 370  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-ral 2819  df-v 3115  df-in 3483  df-ss 3490  df-int 4283
This theorem is referenced by:  ssintab  4299  ssintub  4300  iinpw  4414  trint  4555  oneqmini  4929  fint  5764  sorpssint  6574  iscard2  8357  coftr  8653  isf32lem2  8734  inttsk  9152  isacs1i  14912  mrelatglb  15671  fbfinnfr  20105  fclscmp  20294  dfrtrcl2  28574  fneint  29777  topmeet  29813  igenval2  30094  ismrcd1  30262
  Copyright terms: Public domain W3C validator