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

Theorem intss1 3893
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 2804 . . . 4  |-  x  e. 
_V
21elint 3884 . . 3  |-  ( x  e.  |^| B  <->  A. y
( y  e.  B  ->  x  e.  y ) )
3 eleq1 2356 . . . . . 6  |-  ( y  =  A  ->  (
y  e.  B  <->  A  e.  B ) )
4 eleq2 2357 . . . . . 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 2881 . . . 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 3198 1  |-  ( A  e.  B  ->  |^| B  C_  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1530    = wceq 1632    e. wcel 1696    C_ wss 3165   |^|cint 3878
This theorem is referenced by:  intminss  3904  intmin3  3906  intab  3908  int0el  3909  trint0  4146  intex  4183  oneqmini  4459  onint  4602  onssmin  4604  onnmin  4610  sorpssint  6303  nnawordex  6651  dffi2  7192  inficl  7194  dffi3  7200  tcmin  7442  tc2  7443  rankr1ai  7486  rankuni2b  7541  tcrank  7570  harval2  7646  cfflb  7901  fin23lem20  7979  fin23lem38  7991  isf32lem2  7996  intwun  8373  inttsk  8412  intgru  8452  dfnn2  9775  dfuzi  10118  mremre  13522  isacs1i  13575  mrelatglb  14303  cycsubg  14661  efgrelexlemb  15075  efgcpbllemb  15080  frgpuplem  15097  cssmre  16609  toponmre  16846  1stcfb  17187  ptcnplem  17331  fbssfi  17548  uffix  17632  ufildom1  17637  alexsublem  17754  alexsubALTlem4  17760  tmdgsum2  17795  bcth3  18769  limciun  19260  aalioulem3  19730  shintcli  21924  shsval2i  21982  ococin  22003  chsupsn  22008  insiga  23513  sigagenss  23525  dfrtrcl2  24060  untint  24073  dfon2lem8  24217  dfon2lem9  24218  sltval2  24381  sltres  24389  nodenselem7  24412  nocvxminlem  24415  nobndup  24425  nobnddown  24426  eqintg  25064  intfmu2  25622  clsint2  26350  topmeet  26416  topjoin  26417  heibor1lem  26636  ismrcd1  26876  mzpincl  26915  mzpf  26917  mzpindd  26927  rgspnmin  27479
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-in 3172  df-ss 3179  df-int 3879
  Copyright terms: Public domain W3C validator