Theorem intss1 4916

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 3442	. . . 4 ⊢ 𝑥 ∈ V
2	1	elint 4905	. . 3 ⊢ (𝑥 ∈ ∩ 𝐵 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦))
3		eleq1 2816	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
4		eleq2 2817	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝐴))
5	3, 4	imbi12d 344	. . . . 5 ⊢ (𝑦 = 𝐴 → ((𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) ↔ (𝐴 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
6	5	spcgv 3553	. . . 4 ⊢ (𝐴 ∈ 𝐵 → (∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) → (𝐴 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
7	6	pm2.43a 54	. . 3 ⊢ (𝐴 ∈ 𝐵 → (∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) → 𝑥 ∈ 𝐴))
8	2, 7	biimtrid 242	. 2 ⊢ (𝐴 ∈ 𝐵 → (𝑥 ∈ ∩ 𝐵 → 𝑥 ∈ 𝐴))
9	8	ssrdv 3943	1 ⊢ (𝐴 ∈ 𝐵 → ∩ 𝐵 ⊆ 𝐴)

Syntax hints:   → wi 4  ∀wal 1538   = wceq 1540   ∈ wcel 2109   ⊆ wss 3905  ∩ cint 4899

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-ss 3922  df-int 4900

This theorem is referenced by:  intminss  4927  intmin3  4929  intab  4931  int0el  4932  trintss  5220  intex  5286  intidg  5404  oneqmini  6364  sorpssint  7673  onint  7730  onssmin  7732  onnmin  7738  nnawordex  8562  cofon1  8597  cofonr  8599  dffi2  9332  inficl  9334  dffi3  9340  tcmin  9656  tc2  9657  rankr1ai  9713  rankuni2b  9768  tcrank  9799  harval2  9912  cfflb  10172  fin23lem20  10250  fin23lem38  10262  isf32lem2  10267  intwun  10648  inttsk  10687  intgru  10727  dfnn2  12159  dfuzi  12585  trclubi  14921  trclubgi  14922  trclub  14923  trclubg  14924  cotrtrclfv  14937  trclun  14939  dfrtrcl2  14987  mremre  17524  isacs1i  17581  mrelatglb  18484  cycsubg  19105  efgrelexlemb  19647  efgcpbllemb  19652  frgpuplem  19669  rgspnmin  20518  primefld  20708  cssmre  21618  toponmre  22996  1stcfb  23348  ptcnplem  23524  fbssfi  23740  uffix  23824  ufildom1  23829  alexsublem  23947  alexsubALTlem4  23953  tmdgsum2  23999  bcth3  25247  limciun  25811  aalioulem3  26258  sltval2  27584  sltres  27590  nocvxminlem  27706  eqscut2  27735  scutun12  27739  scutbdaybnd  27744  scutbdaybnd2  27745  scutbdaylt  27747  madebdaylemlrcut  27831  cofcut1  27851  cofcutr  27855  dfn0s2  28247  shintcli  31291  shsval2i  31349  ococin  31370  chsupsn  31375  elrgspnlem4  33195  fldgensdrg  33263  fldgenssv  33264  fldgenssp  33267  insiga  34103  ldsysgenld  34126  ldgenpisyslem2  34130  mclsssvlem  35534  mclsax  35541  mclsind  35542  untint  35684  dfon2lem8  35763  dfon2lem9  35764  clsint2  36302  topmeet  36337  topjoin  36338  heibor1lem  37788  ismrcd1  42671  mzpincl  42707  mzpf  42709  mzpindd  42719  onintunirab  43200  oninfint  43209  clublem  43583  dftrcl3  43693  brtrclfv2  43700  dfrtrcl3  43706  intsaluni  46311  intsal  46312  salgenss  46318  salgencntex  46325  intubeu  48969