Theorem intss1 4939

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 3463	. . . 4 ⊢ 𝑥 ∈ V
2	1	elint 4928	. . 3 ⊢ (𝑥 ∈ ∩ 𝐵 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦))
3		eleq1 2822	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
4		eleq2 2823	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝐴))
5	3, 4	imbi12d 344	. . . . 5 ⊢ (𝑦 = 𝐴 → ((𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) ↔ (𝐴 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
6	5	spcgv 3575	. . . 4 ⊢ (𝐴 ∈ 𝐵 → (∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) → (𝐴 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
7	6	pm2.43a 54	. . 3 ⊢ (𝐴 ∈ 𝐵 → (∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) → 𝑥 ∈ 𝐴))
8	2, 7	biimtrid 242	. 2 ⊢ (𝐴 ∈ 𝐵 → (𝑥 ∈ ∩ 𝐵 → 𝑥 ∈ 𝐴))
9	8	ssrdv 3964	1 ⊢ (𝐴 ∈ 𝐵 → ∩ 𝐵 ⊆ 𝐴)

Syntax hints:   → wi 4  ∀wal 1538   = wceq 1540   ∈ wcel 2108   ⊆ wss 3926  ∩ cint 4922

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-ss 3943  df-int 4923

This theorem is referenced by:  intminss  4950  intmin3  4952  intab  4954  int0el  4955  trintss  5248  intex  5314  intidg  5432  oneqmini  6405  sorpssint  7727  onint  7784  onssmin  7786  onnmin  7792  nnawordex  8649  cofon1  8684  cofonr  8686  dffi2  9435  inficl  9437  dffi3  9443  tcmin  9755  tc2  9756  rankr1ai  9812  rankuni2b  9867  tcrank  9898  harval2  10011  cfflb  10273  fin23lem20  10351  fin23lem38  10363  isf32lem2  10368  intwun  10749  inttsk  10788  intgru  10828  dfnn2  12253  dfuzi  12684  trclubi  15015  trclubgi  15016  trclub  15017  trclubg  15018  cotrtrclfv  15031  trclun  15033  dfrtrcl2  15081  mremre  17616  isacs1i  17669  mrelatglb  18570  cycsubg  19191  efgrelexlemb  19731  efgcpbllemb  19736  frgpuplem  19753  rgspnmin  20575  primefld  20765  cssmre  21653  toponmre  23031  1stcfb  23383  ptcnplem  23559  fbssfi  23775  uffix  23859  ufildom1  23864  alexsublem  23982  alexsubALTlem4  23988  tmdgsum2  24034  bcth3  25283  limciun  25847  aalioulem3  26294  sltval2  27620  sltres  27626  nocvxminlem  27741  eqscut2  27770  scutun12  27774  scutbdaybnd  27779  scutbdaybnd2  27780  scutbdaylt  27782  madebdaylemlrcut  27862  cofcut1  27880  cofcutr  27884  dfn0s2  28276  shintcli  31310  shsval2i  31368  ococin  31389  chsupsn  31394  elrgspnlem4  33240  fldgensdrg  33308  fldgenssv  33309  fldgenssp  33312  insiga  34168  ldsysgenld  34191  ldgenpisyslem2  34195  mclsssvlem  35584  mclsax  35591  mclsind  35592  untint  35729  dfon2lem8  35808  dfon2lem9  35809  clsint2  36347  topmeet  36382  topjoin  36383  heibor1lem  37833  ismrcd1  42721  mzpincl  42757  mzpf  42759  mzpindd  42769  onintunirab  43251  oninfint  43260  clublem  43634  dftrcl3  43744  brtrclfv2  43751  dfrtrcl3  43757  intsaluni  46358  intsal  46359  salgenss  46365  salgencntex  46372  intubeu  48958