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

Theorem intss1 3851
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 2766 . . . 4  |-  x  e. 
_V
21elint 3842 . . 3  |-  ( x  e.  |^| B  <->  A. y
( y  e.  B  ->  x  e.  y ) )
3 eleq1 2318 . . . . . 6  |-  ( y  =  A  ->  (
y  e.  B  <->  A  e.  B ) )
4 eleq2 2319 . . . . . 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 2843 . . . 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 3160 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 3127   |^|cint 3836
This theorem is referenced by:  intminss  3862  intmin3  3864  intab  3866  int0el  3867  trint0  4104  intex  4143  oneqmini  4415  onint  4558  onssmin  4560  onnmin  4566  sorpssint  6221  nnawordex  6603  dffi2  7144  inficl  7146  dffi3  7152  tcmin  7394  tc2  7395  rankr1ai  7438  rankuni2b  7493  tcrank  7522  harval2  7598  cfflb  7853  fin23lem20  7931  fin23lem38  7943  isf32lem2  7948  intwun  8325  inttsk  8364  intgru  8404  dfnn2  9727  dfuzi  10070  mremre  13469  isacs1i  13522  mrelatglb  14250  cycsubg  14608  efgrelexlemb  15022  efgcpbllemb  15027  frgpuplem  15044  cssmre  16556  toponmre  16793  1stcfb  17134  ptcnplem  17278  fbssfi  17495  uffix  17579  ufildom1  17584  alexsublem  17701  alexsubALTlem4  17707  tmdgsum2  17742  bcth3  18716  limciun  19207  aalioulem3  19677  shintcli  21869  shsval2i  21927  ococin  21948  chsupsn  21953  dfrtrcl2  23418  untint  23431  dfon2lem8  23516  dfon2lem9  23517  sltval2  23679  sltres  23687  axdenselem7  23711  nocvxminlem  23714  axfelem9  23724  axfelem10  23725  eqintg  24328  intfmu2  24887  clsint2  25615  topmeet  25681  topjoin  25682  heibor1lem  25901  ismrcd1  26141  mzpincl  26180  mzpf  26182  mzpindd  26192  rgspnmin  26744
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 2239
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 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-v 2765  df-in 3134  df-ss 3141  df-int 3837
  Copyright terms: Public domain W3C validator