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

Syntax hints:   → wi 4  ∀wal 1540   = wceq 1542   ∈ wcel 2114   ⊆ wss 3903  ∩ cint 4904

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-ss 3920  df-int 4905

This theorem is referenced by:  intminss  4931  intmin3  4933  intab  4935  int0el  4936  trintss  5225  intex  5291  intidg  5412  oneqmini  6378  sorpssint  7688  onint  7745  onssmin  7747  onnmin  7753  nnawordex  8575  cofon1  8610  cofonr  8612  dffi2  9338  inficl  9340  dffi3  9346  tcmin  9660  tc2  9661  rankr1ai  9722  rankuni2b  9777  tcrank  9808  harval2  9921  cfflb  10181  fin23lem20  10259  fin23lem38  10271  isf32lem2  10276  intwun  10658  inttsk  10697  intgru  10737  dfnn2  12170  dfuzi  12595  trclubi  14931  trclubgi  14932  trclub  14933  trclubg  14934  cotrtrclfv  14947  trclun  14949  dfrtrcl2  14997  mremre  17535  isacs1i  17592  mrelatglb  18495  cycsubg  19149  efgrelexlemb  19691  efgcpbllemb  19696  frgpuplem  19713  rgspnmin  20560  primefld  20750  cssmre  21660  toponmre  23049  1stcfb  23401  ptcnplem  23577  fbssfi  23793  uffix  23877  ufildom1  23882  alexsublem  24000  alexsubALTlem4  24006  tmdgsum2  24052  bcth3  25299  limciun  25863  aalioulem3  26310  ltsval2  27636  ltsres  27642  nocvxminlem  27762  eqcuts2  27794  cutsun12  27798  cutbdaybnd  27803  cutbdaybnd2  27804  cutbdaylt  27806  madebdaylemlrcut  27907  sltsbday  27925  cofcut1  27928  cofcutr  27932  addonbday  28287  dfn0s2  28340  shintcli  31416  shsval2i  31474  ococin  31495  chsupsn  31500  elrgspnlem4  33338  fldgensdrg  33407  fldgenssv  33408  fldgenssp  33411  insiga  34314  ldsysgenld  34337  ldgenpisyslem2  34341  mclsssvlem  35775  mclsax  35782  mclsind  35783  untint  35925  dfon2lem8  36001  dfon2lem9  36002  clsint2  36542  topmeet  36577  topjoin  36578  heibor1lem  38054  ismrcd1  43049  mzpincl  43085  mzpf  43087  mzpindd  43097  onintunirab  43578  oninfint  43587  clublem  43960  dftrcl3  44070  brtrclfv2  44077  dfrtrcl3  44083  intsaluni  46681  intsal  46682  salgenss  46688  salgencntex  46695  intubeu  49337