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

Theorem intss1 4286
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 3109 . . . 4  |-  x  e. 
_V
21elint 4277 . . 3  |-  ( x  e.  |^| B  <->  A. y
( y  e.  B  ->  x  e.  y ) )
3 eleq1 2526 . . . . . 6  |-  ( y  =  A  ->  (
y  e.  B  <->  A  e.  B ) )
4 eleq2 2527 . . . . . 6  |-  ( y  =  A  ->  (
x  e.  y  <->  x  e.  A ) )
53, 4imbi12d 318 . . . . 5  |-  ( y  =  A  ->  (
( y  e.  B  ->  x  e.  y )  <-> 
( A  e.  B  ->  x  e.  A ) ) )
65spcgv 3191 . . . 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 3495 1  |-  ( A  e.  B  ->  |^| B  C_  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1396    = wceq 1398    e. wcel 1823    C_ wss 3461   |^|cint 4271
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3108  df-in 3468  df-ss 3475  df-int 4272
This theorem is referenced by:  intminss  4298  intmin3  4300  intab  4302  int0el  4303  trint0  4549  intex  4593  oneqmini  4918  sorpssint  6563  onint  6603  onssmin  6605  onnmin  6611  nnawordex  7278  dffi2  7875  inficl  7877  dffi3  7883  tcmin  8163  tc2  8164  rankr1ai  8207  rankuni2b  8262  tcrank  8293  harval2  8369  cfflb  8630  fin23lem20  8708  fin23lem38  8720  isf32lem2  8725  intwun  9102  inttsk  9141  intgru  9181  dfnn2  10544  dfuzi  10949  trclubi  12914  trclubgi  12915  trclub  12916  trclubg  12917  trclfv  12918  trclfvub  12925  cotrtrclfv  12930  trclun  12932  dfrtrcl2  12977  mremre  15093  isacs1i  15146  mrelatglb  16013  cycsubg  16428  efgrelexlemb  16967  efgcpbllemb  16972  frgpuplem  16989  cssmre  18897  toponmre  19761  1stcfb  20112  ptcnplem  20288  fbssfi  20504  uffix  20588  ufildom1  20593  alexsublem  20710  alexsubALTlem4  20716  tmdgsum2  20761  bcth3  21936  limciun  22464  aalioulem3  22896  shintcli  26445  shsval2i  26503  ococin  26524  chsupsn  26529  insiga  28367  mclsssvlem  29186  mclsax  29193  mclsind  29194  untint  29325  dfon2lem8  29462  dfon2lem9  29463  sltval2  29656  sltres  29664  nodenselem7  29687  nocvxminlem  29690  nobndup  29700  nobnddown  29701  clsint2  30387  topmeet  30422  topjoin  30423  heibor1lem  30545  ismrcd1  30870  mzpincl  30906  mzpf  30908  mzpindd  30918  rgspnmin  31361  dftrcl3  38213  dfrtrcl3  38214
  Copyright terms: Public domain W3C validator