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

Theorem intss1 3979
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 2876 . . . 4  |-  x  e. 
_V
21elint 3970 . . 3  |-  ( x  e.  |^| B  <->  A. y
( y  e.  B  ->  x  e.  y ) )
3 eleq1 2426 . . . . . 6  |-  ( y  =  A  ->  (
y  e.  B  <->  A  e.  B ) )
4 eleq2 2427 . . . . . 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 2953 . . . 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 3271 1  |-  ( A  e.  B  ->  |^| B  C_  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1545    = wceq 1647    e. wcel 1715    C_ wss 3238   |^|cint 3964
This theorem is referenced by:  intminss  3990  intmin3  3992  intab  3994  int0el  3995  trint0  4232  intex  4269  oneqmini  4546  onint  4689  onssmin  4691  onnmin  4697  sorpssint  6429  nnawordex  6777  dffi2  7323  inficl  7325  dffi3  7331  tcmin  7573  tc2  7574  rankr1ai  7617  rankuni2b  7672  tcrank  7701  harval2  7777  cfflb  8032  fin23lem20  8110  fin23lem38  8122  isf32lem2  8127  intwun  8504  inttsk  8543  intgru  8583  dfnn2  9906  dfuzi  10253  mremre  13716  isacs1i  13769  mrelatglb  14497  cycsubg  14855  efgrelexlemb  15269  efgcpbllemb  15274  frgpuplem  15291  cssmre  16810  toponmre  17047  1stcfb  17388  ptcnplem  17532  fbssfi  17745  uffix  17829  ufildom1  17834  alexsublem  17951  alexsubALTlem4  17957  tmdgsum2  17992  bcth3  18968  limciun  19459  aalioulem3  19929  shintcli  22342  shsval2i  22400  ococin  22421  chsupsn  22426  insiga  24106  sigagenss  24118  dfrtrcl2  24717  untint  24730  dfon2lem8  24972  dfon2lem9  24973  sltval2  25136  sltres  25144  nodenselem7  25167  nocvxminlem  25170  nobndup  25180  nobnddown  25181  clsint2  25839  topmeet  25905  topjoin  25906  heibor1lem  26124  ismrcd1  26364  mzpincl  26403  mzpf  26405  mzpindd  26415  rgspnmin  26967
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-v 2875  df-in 3245  df-ss 3252  df-int 3965
  Copyright terms: Public domain W3C validator