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

Theorem intss1 3877
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 2791 . . . 4  |-  x  e. 
_V
21elint 3868 . . 3  |-  ( x  e.  |^| B  <->  A. y
( y  e.  B  ->  x  e.  y ) )
3 eleq1 2343 . . . . . 6  |-  ( y  =  A  ->  (
y  e.  B  <->  A  e.  B ) )
4 eleq2 2344 . . . . . 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 2868 . . . 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 3185 1  |-  ( A  e.  B  ->  |^| B  C_  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1527    = wceq 1623    e. wcel 1684    C_ wss 3152   |^|cint 3862
This theorem is referenced by:  intminss  3888  intmin3  3890  intab  3892  int0el  3893  trint0  4130  intex  4167  oneqmini  4443  onint  4586  onssmin  4588  onnmin  4594  sorpssint  6287  nnawordex  6635  dffi2  7176  inficl  7178  dffi3  7184  tcmin  7426  tc2  7427  rankr1ai  7470  rankuni2b  7525  tcrank  7554  harval2  7630  cfflb  7885  fin23lem20  7963  fin23lem38  7975  isf32lem2  7980  intwun  8357  inttsk  8396  intgru  8436  dfnn2  9759  dfuzi  10102  mremre  13506  isacs1i  13559  mrelatglb  14287  cycsubg  14645  efgrelexlemb  15059  efgcpbllemb  15064  frgpuplem  15081  cssmre  16593  toponmre  16830  1stcfb  17171  ptcnplem  17315  fbssfi  17532  uffix  17616  ufildom1  17621  alexsublem  17738  alexsubALTlem4  17744  tmdgsum2  17779  bcth3  18753  limciun  19244  aalioulem3  19714  shintcli  21908  shsval2i  21966  ococin  21987  chsupsn  21992  insiga  23498  sigagenss  23510  dfrtrcl2  24045  untint  24058  dfon2lem8  24146  dfon2lem9  24147  sltval2  24310  sltres  24318  nodenselem7  24341  nocvxminlem  24344  nobndup  24354  nobnddown  24355  eqintg  24961  intfmu2  25519  clsint2  26247  topmeet  26313  topjoin  26314  heibor1lem  26533  ismrcd1  26773  mzpincl  26812  mzpf  26814  mzpindd  26824  rgspnmin  27376
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-in 3159  df-ss 3166  df-int 3863
  Copyright terms: Public domain W3C validator