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

Theorem intss1 3879
Description: An element of a class includes the intersection of the class. Exercise 4 of [TakeutiZaring] p. 44 (with correction), generalized to classes. (Contributed by NM, 18-Nov-1995.)
Assertion
Ref Expression
intss1  |-  ( A  e.  B  ->  |^| B  C_  A )

Proof of Theorem intss1
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vex 2793 . . . 4  |-  x  e. 
_V
21elint 3870 . . 3  |-  ( x  e.  |^| B  <->  A. y
( y  e.  B  ->  x  e.  y ) )
3 eleq1 2345 . . . . . 6  |-  ( y  =  A  ->  (
y  e.  B  <->  A  e.  B ) )
4 eleq2 2346 . . . . . 6  |-  ( y  =  A  ->  (
x  e.  y  <->  x  e.  A ) )
53, 4imbi12d 311 . . . . 5  |-  ( y  =  A  ->  (
( y  e.  B  ->  x  e.  y )  <-> 
( A  e.  B  ->  x  e.  A ) ) )
65spcgv 2870 . . . 4  |-  ( A  e.  B  ->  ( A. y ( y  e.  B  ->  x  e.  y )  ->  ( A  e.  B  ->  x  e.  A ) ) )
76pm2.43a 45 . . 3  |-  ( A  e.  B  ->  ( A. y ( y  e.  B  ->  x  e.  y )  ->  x  e.  A ) )
82, 7syl5bi 208 . 2  |-  ( A  e.  B  ->  (
x  e.  |^| B  ->  x  e.  A ) )
98ssrdv 3187 1  |-  ( A  e.  B  ->  |^| B  C_  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1529    = wceq 1625    e. wcel 1686    C_ wss 3154   |^|cint 3864
This theorem is referenced by:  intminss  3890  intmin3  3892  intab  3894  int0el  3895  trint0  4132  intex  4169  oneqmini  4445  onint  4588  onssmin  4590  onnmin  4596  sorpssint  6289  nnawordex  6637  dffi2  7178  inficl  7180  dffi3  7186  tcmin  7428  tc2  7429  rankr1ai  7472  rankuni2b  7527  tcrank  7556  harval2  7632  cfflb  7887  fin23lem20  7965  fin23lem38  7977  isf32lem2  7982  intwun  8359  inttsk  8398  intgru  8438  dfnn2  9761  dfuzi  10104  mremre  13508  isacs1i  13561  mrelatglb  14289  cycsubg  14647  efgrelexlemb  15061  efgcpbllemb  15066  frgpuplem  15083  cssmre  16595  toponmre  16832  1stcfb  17173  ptcnplem  17317  fbssfi  17534  uffix  17618  ufildom1  17623  alexsublem  17740  alexsubALTlem4  17746  tmdgsum2  17781  bcth3  18755  limciun  19246  aalioulem3  19716  shintcli  21910  shsval2i  21968  ococin  21989  chsupsn  21994  insiga  23500  sigagenss  23512  dfrtrcl2  24047  untint  24060  dfon2lem8  24148  dfon2lem9  24149  sltval2  24312  sltres  24320  nodenselem7  24343  nocvxminlem  24346  nobndup  24356  nobnddown  24357  eqintg  24972  intfmu2  25530  clsint2  26258  topmeet  26324  topjoin  26325  heibor1lem  26544  ismrcd1  26784  mzpincl  26823  mzpf  26825  mzpindd  26835  rgspnmin  27387
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-v 2792  df-in 3161  df-ss 3168  df-int 3865
  Copyright terms: Public domain W3C validator