Theorem intss1 4924

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 3461	. . . 4 ⊢ 𝑥 ∈ V
2	1	elint 4914	. . 3 ⊢ (𝑥 ∈ ∩ 𝐵 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦))
3		eleq1 2853	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
4		eleq2 2854	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝐴))
5	3, 4	imbi12d 347	. . . . 5 ⊢ (𝑦 = 𝐴 → ((𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) ↔ (𝐴 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
6	5	spcgv 3558	. . . 4 ⊢ (𝐴 ∈ 𝐵 → (∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) → (𝐴 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
7	6	pm2.43a 55	. . 3 ⊢ (𝐴 ∈ 𝐵 → (∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) → 𝑥 ∈ 𝐴))
8	2, 7	biimtrid 245	. 2 ⊢ (𝐴 ∈ 𝐵 → (𝑥 ∈ ∩ 𝐵 → 𝑥 ∈ 𝐴))
9	8	ssrdv 3945	1 ⊢ (𝐴 ∈ 𝐵 → ∩ 𝐵 ⊆ 𝐴)

Syntax hints:   → wi 4  ∀wal 1561   = wceq 1563   ∈ wcel 2145   ⊆ wss 3907  ∩ cint 4908

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-ss 3924  df-int 4909

This theorem is referenced by:  intminss  4935  intmin3  4937  intab  4939  int0el  4940  trintss  5231  intex  5305  intidg  5429  oneqmini  6403  sorpssint  7720  onint  7777  onssmin  7779  onnmin  7785  nnawordex  8611  cofon1  8646  cofonr  8648  dffi2  9371  inficl  9373  dffi3  9379  tcmin  9696  tc2  9697  rankr1ai  9758  rankuni2b  9813  tcrank  9844  harval2  9971  cfflb  10231  fin23lem20  10309  fin23lem38  10321  isf32lem2  10326  intwun  10708  inttsk  10747  intgru  10787  dfnn2  12237  dfuzi  12678  trclubi  15023  trclubgi  15024  trclub  15025  trclubg  15026  cotrtrclfv  15039  trclun  15041  dfrtrcl2  15089  mremre  17646  isacs1i  17703  mrelatglb  18606  cycsubg  19270  efgrelexlemb  19811  efgcpbllemb  19816  frgpuplem  19833  rgspnmin  20691  primefld  20877  cssmre  21803  toponmre  23211  1stcfb  23563  ptcnplem  23739  fbssfi  23955  uffix  24039  ufildom1  24044  alexsublem  24162  alexsubALTlem4  24168  tmdgsum2  24214  bcth3  25451  limciun  26014  aalioulem3  26456  ltsval2  27778  ltsres  27784  nocvxminlem  27905  eqcuts2  27937  cutsun12  27941  cutbdaybnd  27946  cutbdaybnd2  27947  cutbdaylt  27949  madebdaylemlrcut  28050  sltsbday  28068  cofcut1  28071  cofcutr  28075  addonbday  28430  dfn0s2  28483  shintcli  31590  shsval2i  31648  ococin  31669  chsupsn  31674  elrgspnlem4  33478  fldgensdrg  33550  fldgenssv  33551  fldgenssp  33554  insiga  34444  ldsysgenld  34467  ldgenpisyslem2  34471  mclsssvlem  35925  mclsax  35932  mclsind  35933  untint  36075  dfon2lem8  36151  dfon2lem9  36152  clsint2  36702  topmeet  36737  topjoin  36738  heibor1lem  38320  ismrcd1  43291  mzpincl  43327  mzpf  43329  mzpindd  43339  onintunirab  43816  oninfint  43825  clublem  44198  dftrcl3  44308  brtrclfv2  44315  dfrtrcl3  44321  intsaluni  46901  intsal  46902  salgenss  46908  salgencntex  46915  intubeu  49613