Theorem intss1 4966

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 3478	. . . 4 ⊢ 𝑥 ∈ V
2	1	elint 4955	. . 3 ⊢ (𝑥 ∈ ∩ 𝐵 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦))
3		eleq1 2821	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
4		eleq2 2822	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝐴))
5	3, 4	imbi12d 344	. . . . 5 ⊢ (𝑦 = 𝐴 → ((𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) ↔ (𝐴 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
6	5	spcgv 3586	. . . 4 ⊢ (𝐴 ∈ 𝐵 → (∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) → (𝐴 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
7	6	pm2.43a 54	. . 3 ⊢ (𝐴 ∈ 𝐵 → (∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) → 𝑥 ∈ 𝐴))
8	2, 7	biimtrid 241	. 2 ⊢ (𝐴 ∈ 𝐵 → (𝑥 ∈ ∩ 𝐵 → 𝑥 ∈ 𝐴))
9	8	ssrdv 3987	1 ⊢ (𝐴 ∈ 𝐵 → ∩ 𝐵 ⊆ 𝐴)

Syntax hints:   → wi 4  ∀wal 1539   = wceq 1541   ∈ wcel 2106   ⊆ wss 3947  ∩ cint 4949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3954  df-ss 3964  df-int 4950

This theorem is referenced by:  intminss  4977  intmin3  4979  intab  4981  int0el  4982  trintss  5283  intex  5336  intidg  5456  oneqmini  6413  sorpssint  7719  onint  7774  onssmin  7776  onnmin  7782  nnawordex  8633  cofon1  8667  cofonr  8669  dffi2  9414  inficl  9416  dffi3  9422  tcmin  9732  tc2  9733  rankr1ai  9789  rankuni2b  9844  tcrank  9875  harval2  9988  cfflb  10250  fin23lem20  10328  fin23lem38  10340  isf32lem2  10345  intwun  10726  inttsk  10765  intgru  10805  dfnn2  12221  dfuzi  12649  trclubi  14939  trclubgi  14940  trclub  14941  trclubg  14942  cotrtrclfv  14955  trclun  14957  dfrtrcl2  15005  mremre  17544  isacs1i  17597  mrelatglb  18509  cycsubg  19079  efgrelexlemb  19612  efgcpbllemb  19617  frgpuplem  19634  primefld  20413  cssmre  21237  toponmre  22588  1stcfb  22940  ptcnplem  23116  fbssfi  23332  uffix  23416  ufildom1  23421  alexsublem  23539  alexsubALTlem4  23545  tmdgsum2  23591  bcth3  24839  limciun  25402  aalioulem3  25838  sltval2  27148  sltres  27154  nocvxminlem  27268  eqscut2  27296  scutun12  27300  scutbdaybnd  27305  scutbdaybnd2  27306  scutbdaylt  27308  madebdaylemlrcut  27382  cofcut1  27396  cofcutr  27400  shintcli  30569  shsval2i  30627  ococin  30648  chsupsn  30653  fldgensdrg  32392  fldgenssv  32393  fldgenssp  32396  insiga  33123  ldsysgenld  33146  ldgenpisyslem2  33150  mclsssvlem  34541  mclsax  34548  mclsind  34549  untint  34669  dfon2lem8  34750  dfon2lem9  34751  clsint2  35202  topmeet  35237  topjoin  35238  heibor1lem  36665  ismrcd1  41421  mzpincl  41457  mzpf  41459  mzpindd  41469  rgspnmin  41898  onintunirab  41961  oninfint  41970  clublem  42346  dftrcl3  42456  brtrclfv2  42463  dfrtrcl3  42469  intsaluni  45031  intsal  45032  salgenss  45038  salgencntex  45045  intubeu  47562