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

Theorem intss1 4065
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 2959 . . . 4  |-  x  e. 
_V
21elint 4056 . . 3  |-  ( x  e.  |^| B  <->  A. y
( y  e.  B  ->  x  e.  y ) )
3 eleq1 2496 . . . . . 6  |-  ( y  =  A  ->  (
y  e.  B  <->  A  e.  B ) )
4 eleq2 2497 . . . . . 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 3036 . . . 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 3354 1  |-  ( A  e.  B  ->  |^| B  C_  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1549    = wceq 1652    e. wcel 1725    C_ wss 3320   |^|cint 4050
This theorem is referenced by:  intminss  4076  intmin3  4078  intab  4080  int0el  4081  trint0  4319  intex  4356  oneqmini  4632  onint  4775  onssmin  4777  onnmin  4783  sorpssint  6532  nnawordex  6880  dffi2  7428  inficl  7430  dffi3  7436  tcmin  7680  tc2  7681  rankr1ai  7724  rankuni2b  7779  tcrank  7808  harval2  7884  cfflb  8139  fin23lem20  8217  fin23lem38  8229  isf32lem2  8234  intwun  8610  inttsk  8649  intgru  8689  dfnn2  10013  dfuzi  10360  mremre  13829  isacs1i  13882  mrelatglb  14610  cycsubg  14968  efgrelexlemb  15382  efgcpbllemb  15387  frgpuplem  15404  cssmre  16920  toponmre  17157  1stcfb  17508  ptcnplem  17653  fbssfi  17869  uffix  17953  ufildom1  17958  alexsublem  18075  alexsubALTlem4  18081  tmdgsum2  18126  bcth3  19284  limciun  19781  aalioulem3  20251  shintcli  22831  shsval2i  22889  ococin  22910  chsupsn  22915  insiga  24520  dfrtrcl2  25148  untint  25161  dfon2lem8  25417  dfon2lem9  25418  sltval2  25611  sltres  25619  nodenselem7  25642  nocvxminlem  25645  nobndup  25655  nobnddown  25656  clsint2  26332  topmeet  26393  topjoin  26394  heibor1lem  26518  ismrcd1  26752  mzpincl  26791  mzpf  26793  mzpindd  26803  rgspnmin  27353
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-v 2958  df-in 3327  df-ss 3334  df-int 4051
  Copyright terms: Public domain W3C validator