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

Theorem intss1 4292
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 3111 . . . 4  |-  x  e. 
_V
21elint 4283 . . 3  |-  ( x  e.  |^| B  <->  A. y
( y  e.  B  ->  x  e.  y ) )
3 eleq1 2534 . . . . . 6  |-  ( y  =  A  ->  (
y  e.  B  <->  A  e.  B ) )
4 eleq2 2535 . . . . . 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 3193 . . . 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 3505 1  |-  ( A  e.  B  ->  |^| B  C_  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1372    = wceq 1374    e. wcel 1762    C_ wss 3471   |^|cint 4277
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2612  df-v 3110  df-in 3478  df-ss 3485  df-int 4278
This theorem is referenced by:  intminss  4303  intmin3  4305  intab  4307  int0el  4308  trint0  4552  intex  4598  oneqmini  4924  sorpssint  6567  onint  6603  onssmin  6605  onnmin  6611  nnawordex  7278  dffi2  7874  inficl  7876  dffi3  7882  tcmin  8163  tc2  8164  rankr1ai  8207  rankuni2b  8262  tcrank  8293  harval2  8369  cfflb  8630  fin23lem20  8708  fin23lem38  8720  isf32lem2  8725  intwun  9104  inttsk  9143  intgru  9183  dfnn2  10540  dfuzi  10942  mremre  14850  isacs1i  14903  mrelatglb  15662  cycsubg  16019  efgrelexlemb  16559  efgcpbllemb  16564  frgpuplem  16581  cssmre  18486  toponmre  19355  1stcfb  19707  ptcnplem  19852  fbssfi  20068  uffix  20152  ufildom1  20157  alexsublem  20274  alexsubALTlem4  20280  tmdgsum2  20325  bcth3  21500  limciun  22028  aalioulem3  22459  shintcli  25911  shsval2i  25969  ococin  25990  chsupsn  25995  insiga  27765  dfrtrcl2  28534  untint  28547  dfon2lem8  28787  dfon2lem9  28788  sltval2  28981  sltres  28989  nodenselem7  29012  nocvxminlem  29015  nobndup  29025  nobnddown  29026  clsint2  29713  topmeet  29774  topjoin  29775  heibor1lem  29897  ismrcd1  30223  mzpincl  30259  mzpf  30261  mzpindd  30271  rgspnmin  30716  trclub  36671  trclubg  36672
  Copyright terms: Public domain W3C validator