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

Theorem intss1 4025
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 2919 . . . 4  |-  x  e. 
_V
21elint 4016 . . 3  |-  ( x  e.  |^| B  <->  A. y
( y  e.  B  ->  x  e.  y ) )
3 eleq1 2464 . . . . . 6  |-  ( y  =  A  ->  (
y  e.  B  <->  A  e.  B ) )
4 eleq2 2465 . . . . . 6  |-  ( y  =  A  ->  (
x  e.  y  <->  x  e.  A ) )
53, 4imbi12d 312 . . . . 5  |-  ( y  =  A  ->  (
( y  e.  B  ->  x  e.  y )  <-> 
( A  e.  B  ->  x  e.  A ) ) )
65spcgv 2996 . . . 4  |-  ( A  e.  B  ->  ( A. y ( y  e.  B  ->  x  e.  y )  ->  ( A  e.  B  ->  x  e.  A ) ) )
76pm2.43a 47 . . 3  |-  ( A  e.  B  ->  ( A. y ( y  e.  B  ->  x  e.  y )  ->  x  e.  A ) )
82, 7syl5bi 209 . 2  |-  ( A  e.  B  ->  (
x  e.  |^| B  ->  x  e.  A ) )
98ssrdv 3314 1  |-  ( A  e.  B  ->  |^| B  C_  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1546    = wceq 1649    e. wcel 1721    C_ wss 3280   |^|cint 4010
This theorem is referenced by:  intminss  4036  intmin3  4038  intab  4040  int0el  4041  trint0  4279  intex  4316  oneqmini  4592  onint  4734  onssmin  4736  onnmin  4742  sorpssint  6491  nnawordex  6839  dffi2  7386  inficl  7388  dffi3  7394  tcmin  7636  tc2  7637  rankr1ai  7680  rankuni2b  7735  tcrank  7764  harval2  7840  cfflb  8095  fin23lem20  8173  fin23lem38  8185  isf32lem2  8190  intwun  8566  inttsk  8605  intgru  8645  dfnn2  9969  dfuzi  10316  mremre  13784  isacs1i  13837  mrelatglb  14565  cycsubg  14923  efgrelexlemb  15337  efgcpbllemb  15342  frgpuplem  15359  cssmre  16875  toponmre  17112  1stcfb  17461  ptcnplem  17606  fbssfi  17822  uffix  17906  ufildom1  17911  alexsublem  18028  alexsubALTlem4  18034  tmdgsum2  18079  bcth3  19237  limciun  19734  aalioulem3  20204  shintcli  22784  shsval2i  22842  ococin  22863  chsupsn  22868  insiga  24473  dfrtrcl2  25101  untint  25114  dfon2lem8  25360  dfon2lem9  25361  sltval2  25524  sltres  25532  nodenselem7  25555  nocvxminlem  25558  nobndup  25568  nobnddown  25569  clsint2  26222  topmeet  26283  topjoin  26284  heibor1lem  26408  ismrcd1  26642  mzpincl  26681  mzpf  26683  mzpindd  26693  rgspnmin  27244
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-in 3287  df-ss 3294  df-int 4011
  Copyright terms: Public domain W3C validator