Theorem intss1 4918

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 3444	. . . 4 ⊢ 𝑥 ∈ V
2	1	elint 4908	. . 3 ⊢ (𝑥 ∈ ∩ 𝐵 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦))
3		eleq1 2824	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
4		eleq2 2825	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝐴))
5	3, 4	imbi12d 344	. . . . 5 ⊢ (𝑦 = 𝐴 → ((𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) ↔ (𝐴 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
6	5	spcgv 3550	. . . 4 ⊢ (𝐴 ∈ 𝐵 → (∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) → (𝐴 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
7	6	pm2.43a 54	. . 3 ⊢ (𝐴 ∈ 𝐵 → (∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) → 𝑥 ∈ 𝐴))
8	2, 7	biimtrid 242	. 2 ⊢ (𝐴 ∈ 𝐵 → (𝑥 ∈ ∩ 𝐵 → 𝑥 ∈ 𝐴))
9	8	ssrdv 3939	1 ⊢ (𝐴 ∈ 𝐵 → ∩ 𝐵 ⊆ 𝐴)

Syntax hints:   → wi 4  ∀wal 1539   = wceq 1541   ∈ wcel 2113   ⊆ wss 3901  ∩ cint 4902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-ss 3918  df-int 4903

This theorem is referenced by:  intminss  4929  intmin3  4931  intab  4933  int0el  4934  trintss  5223  intex  5289  intidg  5405  oneqmini  6370  sorpssint  7678  onint  7735  onssmin  7737  onnmin  7743  nnawordex  8565  cofon1  8600  cofonr  8602  dffi2  9326  inficl  9328  dffi3  9334  tcmin  9648  tc2  9649  rankr1ai  9710  rankuni2b  9765  tcrank  9796  harval2  9909  cfflb  10169  fin23lem20  10247  fin23lem38  10259  isf32lem2  10264  intwun  10646  inttsk  10685  intgru  10725  dfnn2  12158  dfuzi  12583  trclubi  14919  trclubgi  14920  trclub  14921  trclubg  14922  cotrtrclfv  14935  trclun  14937  dfrtrcl2  14985  mremre  17523  isacs1i  17580  mrelatglb  18483  cycsubg  19137  efgrelexlemb  19679  efgcpbllemb  19684  frgpuplem  19701  rgspnmin  20548  primefld  20738  cssmre  21648  toponmre  23037  1stcfb  23389  ptcnplem  23565  fbssfi  23781  uffix  23865  ufildom1  23870  alexsublem  23988  alexsubALTlem4  23994  tmdgsum2  24040  bcth3  25287  limciun  25851  aalioulem3  26298  ltsval2  27624  ltsres  27630  nocvxminlem  27750  eqcuts2  27782  cutsun12  27786  cutbdaybnd  27791  cutbdaybnd2  27792  cutbdaylt  27794  madebdaylemlrcut  27895  sltsbday  27913  cofcut1  27916  cofcutr  27920  addonbday  28275  dfn0s2  28328  shintcli  31404  shsval2i  31462  ococin  31483  chsupsn  31488  elrgspnlem4  33327  fldgensdrg  33396  fldgenssv  33397  fldgenssp  33400  insiga  34294  ldsysgenld  34317  ldgenpisyslem2  34321  mclsssvlem  35756  mclsax  35763  mclsind  35764  untint  35906  dfon2lem8  35982  dfon2lem9  35983  clsint2  36523  topmeet  36558  topjoin  36559  heibor1lem  38006  ismrcd1  42936  mzpincl  42972  mzpf  42974  mzpindd  42984  onintunirab  43465  oninfint  43474  clublem  43847  dftrcl3  43957  brtrclfv2  43964  dfrtrcl3  43970  intsaluni  46569  intsal  46570  salgenss  46576  salgencntex  46583  intubeu  49225