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

Theorem intss1 4131
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 2965 . . . 4  |-  x  e. 
_V
21elint 4122 . . 3  |-  ( x  e.  |^| B  <->  A. y
( y  e.  B  ->  x  e.  y ) )
3 eleq1 2493 . . . . . 6  |-  ( y  =  A  ->  (
y  e.  B  <->  A  e.  B ) )
4 eleq2 2494 . . . . . 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 3046 . . . 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 3350 1  |-  ( A  e.  B  ->  |^| B  C_  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1360    = wceq 1362    e. wcel 1755    C_ wss 3316   |^|cint 4116
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-v 2964  df-in 3323  df-ss 3330  df-int 4117
This theorem is referenced by:  intminss  4142  intmin3  4144  intab  4146  int0el  4147  trint0  4390  intex  4436  oneqmini  4757  sorpssint  6359  onint  6395  onssmin  6397  onnmin  6403  nnawordex  7064  dffi2  7661  inficl  7663  dffi3  7669  tcmin  7949  tc2  7950  rankr1ai  7993  rankuni2b  8048  tcrank  8079  harval2  8155  cfflb  8416  fin23lem20  8494  fin23lem38  8506  isf32lem2  8511  intwun  8889  inttsk  8928  intgru  8968  dfnn2  10322  dfuzi  10719  mremre  14524  isacs1i  14577  mrelatglb  15336  cycsubg  15688  efgrelexlemb  16226  efgcpbllemb  16231  frgpuplem  16248  cssmre  17959  toponmre  18538  1stcfb  18890  ptcnplem  19035  fbssfi  19251  uffix  19335  ufildom1  19340  alexsublem  19457  alexsubALTlem4  19463  tmdgsum2  19508  bcth3  20683  limciun  21210  aalioulem3  21684  shintcli  24554  shsval2i  24612  ococin  24633  chsupsn  24638  insiga  26433  dfrtrcl2  27196  untint  27209  dfon2lem8  27449  dfon2lem9  27450  sltval2  27643  sltres  27651  nodenselem7  27674  nocvxminlem  27677  nobndup  27687  nobnddown  27688  clsint2  28365  topmeet  28426  topjoin  28427  heibor1lem  28549  ismrcd1  28876  mzpincl  28912  mzpf  28914  mzpindd  28924  rgspnmin  29370
  Copyright terms: Public domain W3C validator