Theorem intss1 4920

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 3457	. . . 4 ⊢ 𝑥 ∈ V
2	1	elint 4910	. . 3 ⊢ (𝑥 ∈ ∩ 𝐵 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦))
3		eleq1 2849	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
4		eleq2 2850	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝐴))
5	3, 4	imbi12d 346	. . . . 5 ⊢ (𝑦 = 𝐴 → ((𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) ↔ (𝐴 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
6	5	spcgv 3555	. . . 4 ⊢ (𝐴 ∈ 𝐵 → (∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) → (𝐴 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
7	6	pm2.43a 54	. . 3 ⊢ (𝐴 ∈ 𝐵 → (∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) → 𝑥 ∈ 𝐴))
8	2, 7	biimtrid 244	. 2 ⊢ (𝐴 ∈ 𝐵 → (𝑥 ∈ ∩ 𝐵 → 𝑥 ∈ 𝐴))
9	8	ssrdv 3942	1 ⊢ (𝐴 ∈ 𝐵 → ∩ 𝐵 ⊆ 𝐴)

Syntax hints:   → wi 4  ∀wal 1557   = wceq 1559   ∈ wcel 2141   ⊆ wss 3904  ∩ cint 4904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-ss 3921  df-int 4905

This theorem is referenced by:  intminss  4931  intmin3  4933  intab  4935  int0el  4936  trintss  5225  intex  5299  intidg  5423  oneqmini  6395  sorpssint  7712  onint  7769  onssmin  7771  onnmin  7777  nnawordex  8602  cofon1  8637  cofonr  8639  dffi2  9366  inficl  9368  dffi3  9374  tcmin  9691  tc2  9692  rankr1ai  9753  rankuni2b  9808  tcrank  9839  harval2  9952  cfflb  10213  fin23lem20  10291  fin23lem38  10303  isf32lem2  10308  intwun  10690  inttsk  10729  intgru  10769  dfnn2  12220  dfuzi  12661  trclubi  15006  trclubgi  15007  trclub  15008  trclubg  15009  cotrtrclfv  15022  trclun  15024  dfrtrcl2  15072  mremre  17615  isacs1i  17672  mrelatglb  18575  cycsubg  19232  efgrelexlemb  19773  efgcpbllemb  19778  frgpuplem  19795  rgspnmin  20644  primefld  20834  cssmre  21725  toponmre  23133  1stcfb  23485  ptcnplem  23661  fbssfi  23877  uffix  23961  ufildom1  23966  alexsublem  24084  alexsubALTlem4  24090  tmdgsum2  24136  bcth3  25373  limciun  25936  aalioulem3  26375  ltsval2  27697  ltsres  27703  nocvxminlem  27824  eqcuts2  27856  cutsun12  27860  cutbdaybnd  27865  cutbdaybnd2  27866  cutbdaylt  27868  madebdaylemlrcut  27969  sltsbday  27987  cofcut1  27990  cofcutr  27994  addonbday  28349  dfn0s2  28402  shintcli  31478  shsval2i  31536  ococin  31557  chsupsn  31562  elrgspnlem4  33387  fldgensdrg  33462  fldgenssv  33463  fldgenssp  33466  insiga  34395  ldsysgenld  34418  ldgenpisyslem2  34422  mclsssvlem  35876  mclsax  35883  mclsind  35884  untint  36026  dfon2lem8  36102  dfon2lem9  36103  clsint2  36653  topmeet  36688  topjoin  36689  heibor1lem  38272  ismrcd1  43243  mzpincl  43279  mzpf  43281  mzpindd  43291  onintunirab  43768  oninfint  43777  clublem  44150  dftrcl3  44260  brtrclfv2  44267  dfrtrcl3  44273  intsaluni  46867  intsal  46868  salgenss  46874  salgencntex  46881  intubeu  49569