Theorem intss1 4301

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

Proof of Theorem intss1

Dummy variables are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 3112	. . . 4
2	1	elint 4292	. . 3
3		eleq1 2529	. . . . . 6
4		eleq2 2530	. . . . . 6
5	3, 4	imbi12d 320	. . . . 5
6	5	spcgv 3194	. . . 4
7	6	pm2.43a 49	. . 3
8	2, 7	syl5bi 217	. 2
9	8	ssrdv 3509	1

Syntax hints:  ->wi 4  A.wal 1393  =wceq 1395  e.wcel 1818  C_wss 3475  |^|cint 4286

This theorem is referenced by:  intminss  4313  intmin3  4315  intab  4317  int0el  4318  trint0  4562  intex  4608  oneqmini  4934  sorpssint  6590  onint  6630  onssmin  6632  onnmin  6638  nnawordex  7305  dffi2  7903  inficl  7905  dffi3  7911  tcmin  8193  tc2  8194  rankr1ai  8237  rankuni2b  8292  tcrank  8323  harval2  8399  cfflb  8660  fin23lem20  8738  fin23lem38  8750  isf32lem2  8755  intwun  9134  inttsk  9173  intgru  9213  dfnn2  10574  dfuzi  10978  mremre  15001  isacs1i  15054  mrelatglb  15814  cycsubg  16229  efgrelexlemb  16768  efgcpbllemb  16773  frgpuplem  16790  cssmre  18724  toponmre  19594  1stcfb  19946  ptcnplem  20122  fbssfi  20338  uffix  20422  ufildom1  20427  alexsublem  20544  alexsubALTlem4  20550  tmdgsum2  20595  bcth3  21770  limciun  22298  aalioulem3  22730  shintcli  26247  shsval2i  26305  ococin  26326  chsupsn  26331  insiga  28137  mclsssvlem  28922  mclsax  28929  mclsind  28930  dfrtrcl2  29071  untint  29084  dfon2lem8  29222  dfon2lem9  29223  sltval2  29416  sltres  29424  nodenselem7  29447  nocvxminlem  29450  nobndup  29460  nobnddown  29461  clsint2  30147  topmeet  30182  topjoin  30183  heibor1lem  30305  ismrcd1  30630  mzpincl  30666  mzpf  30668  mzpindd  30678  rgspnmin  31120  trclub  37784  trclubg  37785

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-in 3482  df-ss 3489  df-int 4287