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

Theorem intss1 4164
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 2996 . . . 4  |-  x  e. 
_V
21elint 4155 . . 3  |-  ( x  e.  |^| B  <->  A. y
( y  e.  B  ->  x  e.  y ) )
3 eleq1 2503 . . . . . 6  |-  ( y  =  A  ->  (
y  e.  B  <->  A  e.  B ) )
4 eleq2 2504 . . . . . 6  |-  ( y  =  A  ->  (
x  e.  y  <->  x  e.  A ) )
53, 4imbi12d 320 . . . . 5  |-  ( y  =  A  ->  (
( y  e.  B  ->  x  e.  y )  <-> 
( A  e.  B  ->  x  e.  A ) ) )
65spcgv 3078 . . . 4  |-  ( A  e.  B  ->  ( A. y ( y  e.  B  ->  x  e.  y )  ->  ( A  e.  B  ->  x  e.  A ) ) )
76pm2.43a 49 . . 3  |-  ( A  e.  B  ->  ( A. y ( y  e.  B  ->  x  e.  y )  ->  x  e.  A ) )
82, 7syl5bi 217 . 2  |-  ( A  e.  B  ->  (
x  e.  |^| B  ->  x  e.  A ) )
98ssrdv 3383 1  |-  ( A  e.  B  ->  |^| B  C_  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1367    = wceq 1369    e. wcel 1756    C_ wss 3349   |^|cint 4149
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-v 2995  df-in 3356  df-ss 3363  df-int 4150
This theorem is referenced by:  intminss  4175  intmin3  4177  intab  4179  int0el  4180  trint0  4423  intex  4469  oneqmini  4791  sorpssint  6391  onint  6427  onssmin  6429  onnmin  6435  nnawordex  7097  dffi2  7694  inficl  7696  dffi3  7702  tcmin  7982  tc2  7983  rankr1ai  8026  rankuni2b  8081  tcrank  8112  harval2  8188  cfflb  8449  fin23lem20  8527  fin23lem38  8539  isf32lem2  8544  intwun  8923  inttsk  8962  intgru  9002  dfnn2  10356  dfuzi  10753  mremre  14563  isacs1i  14616  mrelatglb  15375  cycsubg  15730  efgrelexlemb  16268  efgcpbllemb  16273  frgpuplem  16290  cssmre  18140  toponmre  18719  1stcfb  19071  ptcnplem  19216  fbssfi  19432  uffix  19516  ufildom1  19521  alexsublem  19638  alexsubALTlem4  19644  tmdgsum2  19689  bcth3  20864  limciun  21391  aalioulem3  21822  shintcli  24754  shsval2i  24812  ococin  24833  chsupsn  24838  insiga  26602  dfrtrcl2  27372  untint  27385  dfon2lem8  27625  dfon2lem9  27626  sltval2  27819  sltres  27827  nodenselem7  27850  nocvxminlem  27853  nobndup  27863  nobnddown  27864  clsint2  28550  topmeet  28611  topjoin  28612  heibor1lem  28734  ismrcd1  29060  mzpincl  29096  mzpf  29098  mzpindd  29108  rgspnmin  29554
  Copyright terms: Public domain W3C validator