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

Theorem intss 3883
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 70 . . . . 5  |-  ( ( y  e.  A  -> 
y  e.  B )  ->  ( ( y  e.  B  ->  x  e.  y )  ->  (
y  e.  A  ->  x  e.  y )
) )
21al2imi 1548 . . . 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 2791 . . . . 5  |-  x  e. 
_V
43elint 3868 . . . 4  |-  ( x  e.  |^| B  <->  A. y
( y  e.  B  ->  x  e.  y ) )
53elint 3868 . . . 4  |-  ( x  e.  |^| A  <->  A. y
( y  e.  A  ->  x  e.  y ) )
62, 4, 53imtr4g 261 . . 3  |-  ( A. y ( y  e.  A  ->  y  e.  B )  ->  (
x  e.  |^| B  ->  x  e.  |^| A
) )
76alrimiv 1617 . 2  |-  ( A. y ( y  e.  A  ->  y  e.  B )  ->  A. x
( x  e.  |^| B  ->  x  e.  |^| A ) )
8 dfss2 3169 . 2  |-  ( A 
C_  B  <->  A. y
( y  e.  A  ->  y  e.  B ) )
9 dfss2 3169 . 2  |-  ( |^| B  C_  |^| A  <->  A. x
( x  e.  |^| B  ->  x  e.  |^| A ) )
107, 8, 93imtr4i 257 1  |-  ( A 
C_  B  ->  |^| B  C_ 
|^| A )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1527    e. wcel 1684    C_ wss 3152   |^|cint 3862
This theorem is referenced by:  uniintsn  3899  intabs  4172  fiss  7177  tc2  7427  tcss  7429  tcel  7430  rankval4  7539  cfub  7875  cflm  7876  cflecard  7879  fin23lem26  7951  mrcss  13518  lspss  15741  lbsextlem3  15913  aspss  16072  clsss  16791  1stcfb  17171  ufinffr  17624  spanss  21927  pclssN  30083  dochspss  31568
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-v 2790  df-in 3159  df-ss 3166  df-int 3863
  Copyright terms: Public domain W3C validator