Theorem intss1 4922

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 3454	. . . 4 ⊢ 𝑥 ∈ V
2	1	elint 4912	. . 3 ⊢ (𝑥 ∈ ∩ 𝐵 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦))
3		eleq1 2848	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
4		eleq2 2849	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝐴))
5	3, 4	imbi12d 347	. . . . 5 ⊢ (𝑦 = 𝐴 → ((𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) ↔ (𝐴 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
6	5	spcgv 3550	. . . 4 ⊢ (𝐴 ∈ 𝐵 → (∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) → (𝐴 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
7	6	pm2.43a 55	. . 3 ⊢ (𝐴 ∈ 𝐵 → (∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) → 𝑥 ∈ 𝐴))
8	2, 7	biimtrid 245	. 2 ⊢ (𝐴 ∈ 𝐵 → (𝑥 ∈ ∩ 𝐵 → 𝑥 ∈ 𝐴))
9	8	ssrdv 3914	1 ⊢ (𝐴 ∈ 𝐵 → ∩ 𝐵 ⊆ 𝐴)

This proof depends on syntax axioms:   → wi 4  ∀wal 1567   = wceq 1569   ∈ wcel 2144   ⊆ wss 3895  ∩ cint 4906

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-int 4907

This theorem is used by:  intminss  4933  intmin3  4935  intab  4937  int0el  4938  trintss  5230  intex  5304  intidg  5424  oneqmini  6416  sorpssint  7749  onint  7804  onssmin  7806  onnmin  7812  nnawordex  8649  cofon1  8684  cofonr  8686  dffi2  9418  inficl  9420  dffi3  9426  tcmin  9743  tc2  9744  rankr1ai  9809  rankuni2b  9870  tcrank  9904  harval2  10081  cfflb  10340  fin23lem20  10418  fin23lem38  10430  isf32lem2  10435  intwun  10823  inttsk  10862  intgru  10902  dfnn2  12351  dfuzi  12793  trclubi  15154  trclubgi  15155  trclub  15156  trclubg  15157  cotrtrclfv  15170  trclun  15172  dfrtrcl2  15220  mremre  17779  isacs1i  17836  mrelatglb  18739  cycsubg  19428  efgrelexlemb  19969  efgcpbllemb  19974  frgpuplem  19991  rgspnmin  20872  primefld  21067  cssmre  22004  toponmre  23416  1stcfb  23768  ptcnplem  23945  fbssfi  24161  uffix  24245  ufildom1  24250  alexsublem  24368  alexsubALTlem4  24374  tmdgsum2  24420  bcth3  25657  limciun  26219  aalioulem3  26666  ltsval2  28018  ltsres  28024  nocvxminlem  28145  eqcuts2  28177  cutsun12  28181  cutbdaybnd  28186  cutbdaybnd2  28187  cutbdaylt  28189  madebdaylemlrcut  28290  sltsbday  28308  cofcut1  28311  cofcutr  28315  addonbday  28670  dfn0s2  28723  shintcli  31936  shsval2i  31994  ococin  32015  chsupsn  32020  elrgspnlem4  33852  fldgensdrg  33922  fldgenssv  33923  fldgenssp  33926  insiga  34816  ldsysgenld  34839  ldgenpisyslem2  34843  fnfvintima  35762  dfscott3  35797  mclsssvlem  36413  mclsax  36420  mclsind  36421  untint  36569  dfon2lem8  36644  dfon2lem9  36645  clsint2  37209  topmeet  37244  topjoin  37245  heibor1lem  38836  ismrcd1  43802  mzpincl  43838  mzpf  43840  mzpindd  43850  onintunirab  44322  oninfint  44331  clublem  44703  dftrcl3  44813  brtrclfv2  44820  dfrtrcl3  44826  intsaluni  47432  intsal  47433  salgenss  47439  salgencntex  47446  intubeu  50191