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

Theorem intss1 3818
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 2743 . . . 4  |-  x  e. 
_V
21elint 3809 . . 3  |-  ( x  e.  |^| B  <->  A. y
( y  e.  B  ->  x  e.  y ) )
3 eleq1 2316 . . . . . 6  |-  ( y  =  A  ->  (
y  e.  B  <->  A  e.  B ) )
4 eleq2 2317 . . . . . 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 2819 . . . 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 3127 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 3094   |^|cint 3803
This theorem is referenced by:  intminss  3829  intmin3  3831  intab  3833  int0el  3834  trint0  4070  intex  4109  oneqmini  4380  onint  4523  onssmin  4525  onnmin  4531  sorpssint  6186  nnawordex  6568  dffi2  7109  inficl  7111  dffi3  7117  tcmin  7359  tc2  7360  rankr1ai  7403  rankuni2b  7458  tcrank  7487  harval2  7563  cfflb  7818  fin23lem20  7896  fin23lem38  7908  isf32lem2  7913  intwun  8290  inttsk  8329  intgru  8369  dfnn2  9692  dfuzi  10034  mremre  13433  isacs1i  13486  mrelatglb  14214  cycsubg  14572  efgrelexlemb  14986  efgcpbllemb  14991  frgpuplem  15008  cssmre  16520  toponmre  16757  1stcfb  17098  ptcnplem  17242  fbssfi  17459  uffix  17543  ufildom1  17548  alexsublem  17665  alexsubALTlem4  17671  tmdgsum2  17706  bcth3  18680  limciun  19171  aalioulem3  19641  shintcli  21833  shsval2i  21891  ococin  21912  chsupsn  21917  dfrtrcl2  23382  untint  23395  dfon2lem8  23480  dfon2lem9  23481  sltval2  23643  sltres  23651  axdenselem7  23675  nocvxminlem  23678  axfelem9  23688  axfelem10  23689  eqintg  24292  intfmu2  24851  clsint2  25579  topmeet  25645  topjoin  25646  heibor1lem  25865  ismrcd1  26105  mzpincl  26144  mzpf  26146  mzpindd  26156  rgspnmin  26708
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 1927  ax-ext 2237
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 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-v 2742  df-in 3101  df-ss 3108  df-int 3804
  Copyright terms: Public domain W3C validator