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

Theorem intss 4244
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 1607 . . . 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 3068 . . . . 5  |-  x  e. 
_V
43elint 4229 . . . 4  |-  ( x  e.  |^| B  <->  A. y
( y  e.  B  ->  x  e.  y ) )
53elint 4229 . . . 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 1686 . 2  |-  ( A. y ( y  e.  A  ->  y  e.  B )  ->  A. x
( x  e.  |^| B  ->  x  e.  |^| A ) )
8 dfss2 3440 . 2  |-  ( A 
C_  B  <->  A. y
( y  e.  A  ->  y  e.  B ) )
9 dfss2 3440 . 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 1368    e. wcel 1758    C_ wss 3423   |^|cint 4223
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2599  df-v 3067  df-in 3430  df-ss 3437  df-int 4224
This theorem is referenced by:  uniintsn  4260  intabs  4548  fiss  7772  tc2  8060  tcss  8062  tcel  8063  rankval4  8172  cfub  8516  cflm  8517  cflecard  8520  fin23lem26  8592  mrcss  14653  lspss  17168  lbsextlem3  17344  aspss  17506  clsss  18771  1stcfb  19162  ufinffr  19615  spanss  24883  pclssN  33841  dochspss  35326
  Copyright terms: Public domain W3C validator