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

Theorem intss1 3878
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 2792 . . . 4  |-  x  e. 
_V
21elint 3869 . . 3  |-  ( x  e.  |^| B  <->  A. y
( y  e.  B  ->  x  e.  y ) )
3 eleq1 2344 . . . . . 6  |-  ( y  =  A  ->  (
y  e.  B  <->  A  e.  B ) )
4 eleq2 2345 . . . . . 6  |-  ( y  =  A  ->  (
x  e.  y  <->  x  e.  A ) )
53, 4imbi12d 311 . . . . 5  |-  ( y  =  A  ->  (
( y  e.  B  ->  x  e.  y )  <-> 
( A  e.  B  ->  x  e.  A ) ) )
65spcgv 2869 . . . 4  |-  ( A  e.  B  ->  ( A. y ( y  e.  B  ->  x  e.  y )  ->  ( A  e.  B  ->  x  e.  A ) ) )
76pm2.43a 45 . . 3  |-  ( A  e.  B  ->  ( A. y ( y  e.  B  ->  x  e.  y )  ->  x  e.  A ) )
82, 7syl5bi 208 . 2  |-  ( A  e.  B  ->  (
x  e.  |^| B  ->  x  e.  A ) )
98ssrdv 3186 1  |-  ( A  e.  B  ->  |^| B  C_  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1527    = wceq 1623    e. wcel 1685    C_ wss 3153   |^|cint 3863
This theorem is referenced by:  intminss  3889  intmin3  3891  intab  3893  int0el  3894  trint0  4131  intex  4170  oneqmini  4442  onint  4585  onssmin  4587  onnmin  4593  sorpssint  6249  nnawordex  6631  dffi2  7172  inficl  7174  dffi3  7180  tcmin  7422  tc2  7423  rankr1ai  7466  rankuni2b  7521  tcrank  7550  harval2  7626  cfflb  7881  fin23lem20  7959  fin23lem38  7971  isf32lem2  7976  intwun  8353  inttsk  8392  intgru  8432  dfnn2  9755  dfuzi  10098  mremre  13502  isacs1i  13555  mrelatglb  14283  cycsubg  14641  efgrelexlemb  15055  efgcpbllemb  15060  frgpuplem  15077  cssmre  16589  toponmre  16826  1stcfb  17167  ptcnplem  17311  fbssfi  17528  uffix  17612  ufildom1  17617  alexsublem  17734  alexsubALTlem4  17740  tmdgsum2  17775  bcth3  18749  limciun  19240  aalioulem3  19710  shintcli  21904  shsval2i  21962  ococin  21983  chsupsn  21988  dfrtrcl2  23452  untint  23465  dfon2lem8  23550  dfon2lem9  23551  sltval2  23713  sltres  23721  axdenselem7  23745  nocvxminlem  23748  axfelem9  23758  axfelem10  23759  eqintg  24371  intfmu2  24930  clsint2  25658  topmeet  25724  topjoin  25725  heibor1lem  25944  ismrcd1  26184  mzpincl  26223  mzpf  26225  mzpindd  26235  rgspnmin  26787
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1636  ax-8 1644  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1631  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-v 2791  df-in 3160  df-ss 3167  df-int 3864
  Copyright terms: Public domain W3C validator