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

Theorem intss1 4241
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 3034 . . . 4  |-  x  e. 
_V
21elint 4232 . . 3  |-  ( x  e.  |^| B  <->  A. y
( y  e.  B  ->  x  e.  y ) )
3 eleq1 2537 . . . . . 6  |-  ( y  =  A  ->  (
y  e.  B  <->  A  e.  B ) )
4 eleq2 2538 . . . . . 6  |-  ( y  =  A  ->  (
x  e.  y  <->  x  e.  A ) )
53, 4imbi12d 327 . . . . 5  |-  ( y  =  A  ->  (
( y  e.  B  ->  x  e.  y )  <-> 
( A  e.  B  ->  x  e.  A ) ) )
65spcgv 3120 . . . 4  |-  ( A  e.  B  ->  ( A. y ( y  e.  B  ->  x  e.  y )  ->  ( A  e.  B  ->  x  e.  A ) ) )
76pm2.43a 50 . . 3  |-  ( A  e.  B  ->  ( A. y ( y  e.  B  ->  x  e.  y )  ->  x  e.  A ) )
82, 7syl5bi 225 . 2  |-  ( A  e.  B  ->  (
x  e.  |^| B  ->  x  e.  A ) )
98ssrdv 3424 1  |-  ( A  e.  B  ->  |^| B  C_  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1450    = wceq 1452    e. wcel 1904    C_ wss 3390   |^|cint 4226
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451
This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-v 3033  df-in 3397  df-ss 3404  df-int 4227
This theorem is referenced by:  intminss  4252  intmin3  4254  intab  4256  int0el  4257  trint0  4507  intex  4557  oneqmini  5481  sorpssint  6600  onint  6641  onssmin  6643  onnmin  6649  nnawordex  7356  dffi2  7955  inficl  7957  dffi3  7963  tcmin  8243  tc2  8244  rankr1ai  8287  rankuni2b  8342  tcrank  8373  harval2  8449  cfflb  8707  fin23lem20  8785  fin23lem38  8797  isf32lem2  8802  intwun  9178  inttsk  9217  intgru  9257  dfnn2  10644  dfuzi  11049  trclubi  13135  trclubiOLD  13136  trclubgi  13137  trclubgiOLD  13138  trclub  13139  trclubg  13140  cotrtrclfv  13153  trclun  13155  dfrtrcl2  13202  mremre  15588  isacs1i  15641  mrelatglb  16508  cycsubg  16923  efgrelexlemb  17478  efgcpbllemb  17483  frgpuplem  17500  cssmre  19333  toponmre  20186  1stcfb  20537  ptcnplem  20713  fbssfi  20930  uffix  21014  ufildom1  21019  alexsublem  21137  alexsubALTlem4  21143  tmdgsum2  21189  bcth3  22377  limciun  22928  aalioulem3  23369  shintcli  27063  shsval2i  27121  ococin  27142  chsupsn  27147  insiga  29033  ldsysgenld  29056  ldgenpisyslem2  29060  mclsssvlem  30272  mclsax  30279  mclsind  30280  untint  30411  dfon2lem8  30507  dfon2lem9  30508  sltval2  30614  sltres  30622  nodenselem7  30647  nocvxminlem  30650  nobndup  30660  nobnddown  30661  clsint2  31056  topmeet  31091  topjoin  31092  heibor1lem  32205  ismrcd1  35611  mzpincl  35647  mzpf  35649  mzpindd  35659  rgspnmin  36108  clublem  36288  dftrcl3  36383  brtrclfv2  36390  dfrtrcl3  36396  intsaluni  38300  intsal  38301  salgenss  38307  salgencntex  38314
  Copyright terms: Public domain W3C validator