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

Theorem intss 4303
Description: Intersection of subclasses. (Contributed by NM, 14-Oct-1999.)
Assertion
Ref Expression
intss  |-  ( A 
C_  B  ->  |^| B  C_ 
|^| A )

Proof of Theorem intss
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 imim1 76 . . . . 5  |-  ( ( y  e.  A  -> 
y  e.  B )  ->  ( ( y  e.  B  ->  x  e.  y )  ->  (
y  e.  A  ->  x  e.  y )
) )
21al2imi 1616 . . . 4  |-  ( A. y ( y  e.  A  ->  y  e.  B )  ->  ( A. y ( y  e.  B  ->  x  e.  y )  ->  A. y
( y  e.  A  ->  x  e.  y ) ) )
3 vex 3116 . . . . 5  |-  x  e. 
_V
43elint 4288 . . . 4  |-  ( x  e.  |^| B  <->  A. y
( y  e.  B  ->  x  e.  y ) )
53elint 4288 . . . 4  |-  ( x  e.  |^| A  <->  A. y
( y  e.  A  ->  x  e.  y ) )
62, 4, 53imtr4g 270 . . 3  |-  ( A. y ( y  e.  A  ->  y  e.  B )  ->  (
x  e.  |^| B  ->  x  e.  |^| A
) )
76alrimiv 1695 . 2  |-  ( A. y ( y  e.  A  ->  y  e.  B )  ->  A. x
( x  e.  |^| B  ->  x  e.  |^| A ) )
8 dfss2 3493 . 2  |-  ( A 
C_  B  <->  A. y
( y  e.  A  ->  y  e.  B ) )
9 dfss2 3493 . 2  |-  ( |^| B  C_  |^| A  <->  A. x
( x  e.  |^| B  ->  x  e.  |^| A ) )
107, 8, 93imtr4i 266 1  |-  ( A 
C_  B  ->  |^| B  C_ 
|^| A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1377    e. wcel 1767    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-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-v 3115  df-in 3483  df-ss 3490  df-int 4283
This theorem is referenced by:  uniintsn  4319  intabs  4608  fiss  7880  tc2  8169  tcss  8171  tcel  8172  rankval4  8281  cfub  8625  cflm  8626  cflecard  8629  fin23lem26  8701  mrcss  14864  lspss  17410  lbsextlem3  17586  aspss  17749  clsss  19318  1stcfb  19709  ufinffr  20162  spanss  25939  pclssN  34690  dochspss  36175
  Copyright terms: Public domain W3C validator