Theorem intss1 4926

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 3458	. . . 4 ⊢ 𝑥 ∈ V
2	1	elint 4916	. . 3 ⊢ (𝑥 ∈ ∩ 𝐵 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦))
3		eleq1 2852	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
4		eleq2 2853	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝐴))
5	3, 4	imbi12d 347	. . . . 5 ⊢ (𝑦 = 𝐴 → ((𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) ↔ (𝐴 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
6	5	spcgv 3554	. . . 4 ⊢ (𝐴 ∈ 𝐵 → (∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) → (𝐴 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
7	6	pm2.43a 55	. . 3 ⊢ (𝐴 ∈ 𝐵 → (∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) → 𝑥 ∈ 𝐴))
8	2, 7	biimtrid 245	. 2 ⊢ (𝐴 ∈ 𝐵 → (𝑥 ∈ ∩ 𝐵 → 𝑥 ∈ 𝐴))
9	8	ssrdv 3919	1 ⊢ (𝐴 ∈ 𝐵 → ∩ 𝐵 ⊆ 𝐴)

This proof depends on syntax axioms:   → wi 4  ∀wal 1568   = wceq 1570   ∈ wcel 2147   ⊆ wss 3900  ∩ cint 4910

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-int 4911

This theorem is used by:  intminss  4937  intmin3  4939  intab  4941  int0el  4942  trintss  5234  intex  5309  intidg  5429  oneqmini  6434  sorpssint  7773  onint  7828  onssmin  7830  onnmin  7836  nnawordex  8674  cofon1  8709  cofonr  8711  dffi2  9442  inficl  9444  dffi3  9450  tcmin  9767  tc2  9768  rankr1ai  9833  rankuni2b  9894  tcrank  9928  harval2  10105  cfflb  10364  fin23lem20  10442  fin23lem38  10454  isf32lem2  10459  intwun  10847  inttsk  10886  intgru  10926  dfnn2  12375  dfuzi  12817  trclubi  15178  trclubgi  15179  trclub  15180  trclubg  15181  cotrtrclfv  15194  trclun  15196  dfrtrcl2  15244  mremre  17803  isacs1i  17860  mrelatglb  18763  cycsubg  19452  efgrelexlemb  19994  efgcpbllemb  19999  frgpuplem  20016  rgspnmin  20897  primefld  21092  cssmre  22029  toponmre  23441  1stcfb  23793  ptcnplem  23970  fbssfi  24186  uffix  24270  ufildom1  24275  alexsublem  24393  alexsubALTlem4  24399  tmdgsum2  24445  bcth3  25682  limciun  26244  aalioulem3  26691  ltsval2  28043  ltsres  28049  nocvxminlem  28170  eqcuts2  28202  cutsun12  28206  cutbdaybnd  28211  cutbdaybnd2  28212  cutbdaylt  28214  madebdaylemlrcut  28315  sltsbday  28333  cofcut1  28336  cofcutr  28340  addonbday  28695  dfn0s2  28748  shintcli  31961  shsval2i  32019  ococin  32040  chsupsn  32045  elrgspnlem4  33876  fldgensdrg  33946  fldgenssv  33947  fldgenssp  33950  insiga  34840  ldsysgenld  34863  ldgenpisyslem2  34867  fnfvintima  35786  dfscott3  35827  mclsssvlem  36494  mclsax  36501  mclsind  36502  untint  36655  dfon2lem8  36730  dfon2lem9  36731  clsint2  37295  topmeet  37330  topjoin  37331  heibor1lem  38935  ismrcd1  43902  mzpincl  43938  mzpf  43940  mzpindd  43950  onintunirab  44421  oninfint  44430  clublem  44802  dftrcl3  44912  brtrclfv2  44919  dfrtrcl3  44925  intsaluni  47544  intsal  47545  salgenss  47551  salgencntex  47558  intubeu  50303