Theorem intss1 4896

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 3437	. . . 4 ⊢ 𝑥 ∈ V
2	1	elint 4886	. . 3 ⊢ (𝑥 ∈ ∩ 𝐵 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦))
3		eleq1 2829	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
4		eleq2 2830	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝐴))
5	3, 4	imbi12d 346	. . . . 5 ⊢ (𝑦 = 𝐴 → ((𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) ↔ (𝐴 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
6	5	spcgv 3536	. . . 4 ⊢ (𝐴 ∈ 𝐵 → (∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) → (𝐴 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
7	6	pm2.43a 54	. . 3 ⊢ (𝐴 ∈ 𝐵 → (∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) → 𝑥 ∈ 𝐴))
8	2, 7	biimtrid 244	. 2 ⊢ (𝐴 ∈ 𝐵 → (𝑥 ∈ ∩ 𝐵 → 𝑥 ∈ 𝐴))
9	8	ssrdv 3923	1 ⊢ (𝐴 ∈ 𝐵 → ∩ 𝐵 ⊆ 𝐴)

Syntax hints:   → wi 4  ∀wal 1546   = wceq 1548   ∈ wcel 2121   ⊆ wss 3885  ∩ cint 4880

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-v 3435  df-ss 3902  df-int 4881

This theorem is referenced by:  intminss  4907  intmin3  4909  intab  4911  int0el  4912  trintss  5201  intex  5275  intidg  5399  oneqmini  6367  sorpssint  7680  onint  7737  onssmin  7739  onnmin  7745  nnawordex  8567  cofon1  8602  cofonr  8604  dffi2  9330  inficl  9332  dffi3  9338  tcmin  9655  tc2  9656  rankr1ai  9717  rankuni2b  9772  tcrank  9803  harval2  9916  cfflb  10176  fin23lem20  10254  fin23lem38  10266  isf32lem2  10271  intwun  10653  inttsk  10692  intgru  10732  dfnn2  12182  dfuzi  12615  trclubi  14953  trclubgi  14954  trclub  14955  trclubg  14956  cotrtrclfv  14969  trclun  14971  dfrtrcl2  15019  mremre  17561  isacs1i  17618  mrelatglb  18521  cycsubg  19178  efgrelexlemb  19720  efgcpbllemb  19725  frgpuplem  19742  rgspnmin  20591  primefld  20781  cssmre  21672  toponmre  23080  1stcfb  23432  ptcnplem  23608  fbssfi  23824  uffix  23908  ufildom1  23913  alexsublem  24031  alexsubALTlem4  24037  tmdgsum2  24083  bcth3  25320  limciun  25883  aalioulem3  26322  ltsval2  27642  ltsres  27648  nocvxminlem  27768  eqcuts2  27800  cutsun12  27804  cutbdaybnd  27809  cutbdaybnd2  27810  cutbdaylt  27812  madebdaylemlrcut  27913  sltsbday  27931  cofcut1  27934  cofcutr  27938  addonbday  28293  dfn0s2  28346  shintcli  31422  shsval2i  31480  ococin  31501  chsupsn  31506  elrgspnlem4  33330  fldgensdrg  33402  fldgenssv  33403  fldgenssp  33406  insiga  34333  ldsysgenld  34356  ldgenpisyslem2  34360  mclsssvlem  35805  mclsax  35812  mclsind  35813  untint  35955  dfon2lem8  36031  dfon2lem9  36032  clsint2  36572  topmeet  36607  topjoin  36608  heibor1lem  38191  ismrcd1  43162  mzpincl  43198  mzpf  43200  mzpindd  43210  onintunirab  43687  oninfint  43696  clublem  44069  dftrcl3  44179  brtrclfv2  44186  dfrtrcl3  44192  intsaluni  46786  intsal  46787  salgenss  46793  salgencntex  46800  intubeu  49488