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

Theorem intss 4309
Description: Intersection of subclasses. (Contributed by NM, 14-Oct-1999.) (Proof shortened by OpenAI, 25-Mar-2020.)
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 ssralv 3560 . . 3  |-  ( A 
C_  B  ->  ( A. x  e.  B  y  e.  x  ->  A. x  e.  A  y  e.  x ) )
21ss2abdv 3569 . 2  |-  ( A 
C_  B  ->  { y  |  A. x  e.  B  y  e.  x }  C_  { y  | 
A. x  e.  A  y  e.  x }
)
3 dfint2 4290 . 2  |-  |^| B  =  { y  |  A. x  e.  B  y  e.  x }
4 dfint2 4290 . 2  |-  |^| A  =  { y  |  A. x  e.  A  y  e.  x }
52, 3, 43sstr4g 3540 1  |-  ( A 
C_  B  ->  |^| B  C_ 
|^| A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1819   {cab 2442   A.wral 2807    C_ wss 3471   |^|cint 4288
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812  df-in 3478  df-ss 3485  df-int 4289
This theorem is referenced by:  uniintsn  4326  intabs  4617  fiss  7902  tc2  8190  tcss  8192  tcel  8193  rankval4  8302  cfub  8646  cflm  8647  cflecard  8650  fin23lem26  8722  mrcss  15033  lspss  17757  lbsextlem3  17933  aspss  18108  clsss  19682  1stcfb  20072  ufinffr  20556  spanss  26393  ss2mcls  29125  pclssN  35761  dochspss  37248  clsslem  37947
  Copyright terms: Public domain W3C validator