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

Theorem intss1 3775
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
StepHypRef Expression
1 vex 2730 . . . 4  |-  x  e. 
_V
21elint 3766 . . 3  |-  ( x  e.  |^| B  <->  A. y
( y  e.  B  ->  x  e.  y ) )
3 eleq1 2313 . . . . . 6  |-  ( y  =  A  ->  (
y  e.  B  <->  A  e.  B ) )
4 eleq2 2314 . . . . . 6  |-  ( y  =  A  ->  (
x  e.  y  <->  x  e.  A ) )
53, 4imbi12d 313 . . . . 5  |-  ( y  =  A  ->  (
( y  e.  B  ->  x  e.  y )  <-> 
( A  e.  B  ->  x  e.  A ) ) )
65cla4gv 2805 . . . 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 210 . 2  |-  ( A  e.  B  ->  (
x  e.  |^| B  ->  x  e.  A ) )
98ssrdv 3106 1  |-  ( A  e.  B  ->  |^| B  C_  A )
Colors of variables: wff set class
Syntax hints:    -> wi 6   A.wal 1532    = wceq 1619    e. wcel 1621    C_ wss 3078   |^|cint 3760
This theorem is referenced by:  intminss  3786  intmin3  3788  intab  3790  int0el  3791  trint0  4027  intex  4065  oneqmini  4336  onint  4477  onssmin  4479  onnmin  4485  sorpssint  6139  nnawordex  6521  dffi2  7060  inficl  7062  dffi3  7068  tcmin  7310  tc2  7311  rankr1ai  7354  rankuni2b  7409  tcrank  7438  harval2  7514  cfflb  7769  fin23lem20  7847  fin23lem38  7859  isf32lem2  7864  intwun  8237  inttsk  8276  intgru  8316  dfnn2  9639  dfuzi  9981  mremre  13378  isacs1i  13403  mrelatglb  14122  cycsubg  14480  efgrelexlemb  14894  efgcpbllemb  14899  frgpuplem  14916  cssmre  16425  toponmre  16662  1stcfb  17003  ptcnplem  17147  fbssfi  17364  uffix  17448  ufildom1  17453  alexsublem  17570  alexsubALTlem4  17576  tmdgsum2  17611  bcth3  18585  limciun  19076  aalioulem3  19546  shintcli  21738  shsval2i  21796  ococin  21817  chsupsn  21822  dfrtrcl2  23216  untint  23229  dfon2lem8  23314  dfon2lem9  23315  sltval2  23477  sltres  23485  axdenselem7  23509  nocvxminlem  23512  axfelem9  23522  axfelem10  23523  eqintg  24126  intfmu2  24685  clsint2  25413  topmeet  25479  topjoin  25480  heibor1lem  25699  ismrcd1  25939  mzpincl  25978  mzpf  25980  mzpindd  25990  rgspnmin  26542
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-v 2729  df-in 3085  df-ss 3089  df-int 3761
  Copyright terms: Public domain W3C validator