Theorem intss1 4929

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 3459	. . . 4 ⊢ 𝑥 ∈ V
2	1	elint 4919	. . 3 ⊢ (𝑥 ∈ ∩ 𝐵 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦))
3		eleq1 2851	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
4		eleq2 2852	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝐴))
5	3, 4	imbi12d 347	. . . . 5 ⊢ (𝑦 = 𝐴 → ((𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) ↔ (𝐴 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
6	5	spcgv 3556	. . . 4 ⊢ (𝐴 ∈ 𝐵 → (∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) → (𝐴 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
7	6	pm2.43a 55	. . 3 ⊢ (𝐴 ∈ 𝐵 → (∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) → 𝑥 ∈ 𝐴))
8	2, 7	biimtrid 245	. 2 ⊢ (𝐴 ∈ 𝐵 → (𝑥 ∈ ∩ 𝐵 → 𝑥 ∈ 𝐴))
9	8	ssrdv 3944	1 ⊢ (𝐴 ∈ 𝐵 → ∩ 𝐵 ⊆ 𝐴)

Syntax hints:   → wi 4  ∀wal 1568   = wceq 1570   ∈ wcel 2143   ⊆ wss 3906  ∩ cint 4913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-ss 3923  df-int 4914

This theorem is referenced by:  intminss  4940  intmin3  4942  intab  4944  int0el  4945  trintss  5238  intex  5316  intidg  5440  oneqmini  6416  sorpssint  7732  onint  7790  onssmin  7792  onnmin  7798  nnawordex  8624  cofon1  8659  cofonr  8661  dffi2  9384  inficl  9386  dffi3  9392  tcmin  9709  tc2  9710  rankr1ai  9771  rankuni2b  9826  tcrank  9857  harval2  9984  cfflb  10244  fin23lem20  10322  fin23lem38  10334  isf32lem2  10339  intwun  10721  inttsk  10760  intgru  10800  dfnn2  12247  dfuzi  12688  trclubi  15035  trclubgi  15036  trclub  15037  trclubg  15038  cotrtrclfv  15051  trclun  15053  dfrtrcl2  15101  mremre  17657  isacs1i  17714  mrelatglb  18617  cycsubg  19280  efgrelexlemb  19821  efgcpbllemb  19826  frgpuplem  19843  rgspnmin  20701  primefld  20889  cssmre  21824  toponmre  23231  1stcfb  23583  ptcnplem  23759  fbssfi  23975  uffix  24059  ufildom1  24064  alexsublem  24182  alexsubALTlem4  24188  tmdgsum2  24234  bcth3  25471  limciun  26034  aalioulem3  26476  ltsval2  27798  ltsres  27804  nocvxminlem  27925  eqcuts2  27957  cutsun12  27961  cutbdaybnd  27966  cutbdaybnd2  27967  cutbdaylt  27969  madebdaylemlrcut  28070  sltsbday  28088  cofcut1  28091  cofcutr  28095  addonbday  28450  dfn0s2  28503  shintcli  31659  shsval2i  31717  ococin  31738  chsupsn  31743  elrgspnlem4  33543  fldgensdrg  33613  fldgenssv  33614  fldgenssp  33617  insiga  34505  ldsysgenld  34528  ldgenpisyslem2  34532  fnfvintima  35454  dfscott3  35490  mclsssvlem  36032  mclsax  36039  mclsind  36040  untint  36182  dfon2lem8  36258  dfon2lem9  36259  clsint2  36818  topmeet  36853  topjoin  36854  heibor1lem  38438  ismrcd1  43409  mzpincl  43445  mzpf  43447  mzpindd  43457  onintunirab  43934  oninfint  43943  clublem  44316  dftrcl3  44426  brtrclfv2  44433  dfrtrcl3  44439  intsaluni  47023  intsal  47024  salgenss  47030  salgencntex  47037  intubeu  49739