Theorem intss1 4933

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 3462	. . . 4 ⊢ 𝑥 ∈ V
2	1	elint 4923	. . 3 ⊢ (𝑥 ∈ ∩ 𝐵 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦))
3		eleq1 2854	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
4		eleq2 2855	. . . . . 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 3946	1 ⊢ (𝐴 ∈ 𝐵 → ∩ 𝐵 ⊆ 𝐴)

This proof depends on syntax axioms:   → wi 4  ∀wal 1568   = wceq 1570   ∈ wcel 2146   ⊆ wss 3908  ∩ cint 4917

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-ss 3925  df-int 4918

This theorem is used by:  intminss  4944  intmin3  4946  intab  4948  int0el  4949  trintss  5242  intex  5319  intidg  5443  oneqmini  6421  sorpssint  7743  onint  7798  onssmin  7800  onnmin  7806  nnawordex  8632  cofon1  8667  cofonr  8669  dffi2  9393  inficl  9395  dffi3  9401  tcmin  9718  tc2  9719  rankr1ai  9780  rankuni2b  9835  tcrank  9866  harval2  10002  cfflb  10261  fin23lem20  10339  fin23lem38  10351  isf32lem2  10356  intwun  10738  inttsk  10777  intgru  10817  dfnn2  12264  dfuzi  12705  trclubi  15059  trclubgi  15060  trclub  15061  trclubg  15062  cotrtrclfv  15075  trclun  15077  dfrtrcl2  15125  mremre  17681  isacs1i  17738  mrelatglb  18641  cycsubg  19310  efgrelexlemb  19851  efgcpbllemb  19856  frgpuplem  19873  rgspnmin  20751  primefld  20945  cssmre  21880  toponmre  23287  1stcfb  23639  ptcnplem  23815  fbssfi  24031  uffix  24115  ufildom1  24120  alexsublem  24238  alexsubALTlem4  24244  tmdgsum2  24290  bcth3  25527  limciun  26090  aalioulem3  26534  ltsval2  27857  ltsres  27863  nocvxminlem  27984  eqcuts2  28016  cutsun12  28020  cutbdaybnd  28025  cutbdaybnd2  28026  cutbdaylt  28028  madebdaylemlrcut  28129  sltsbday  28147  cofcut1  28150  cofcutr  28154  addonbday  28509  dfn0s2  28562  shintcli  31718  shsval2i  31776  ococin  31797  chsupsn  31802  elrgspnlem4  33596  fldgensdrg  33666  fldgenssv  33667  fldgenssp  33670  insiga  34559  ldsysgenld  34582  ldgenpisyslem2  34586  fnfvintima  35502  dfscott3  35537  mclsssvlem  36075  mclsax  36082  mclsind  36083  untint  36225  dfon2lem8  36301  dfon2lem9  36302  clsint2  36881  topmeet  36916  topjoin  36917  heibor1lem  38501  ismrcd1  43470  mzpincl  43506  mzpf  43508  mzpindd  43518  onintunirab  43995  oninfint  44004  clublem  44377  dftrcl3  44487  brtrclfv2  44494  dfrtrcl3  44500  intsaluni  47084  intsal  47085  salgenss  47091  salgencntex  47098  intubeu  49803