Theorem intss1 4927

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

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

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 3449  df-ss 3931  df-int 4911

This theorem is referenced by:  intminss  4938  intmin3  4940  intab  4942  int0el  4943  trintss  5233  intex  5299  intidg  5417  oneqmini  6385  sorpssint  7709  onint  7766  onssmin  7768  onnmin  7774  nnawordex  8601  cofon1  8636  cofonr  8638  dffi2  9374  inficl  9376  dffi3  9382  tcmin  9694  tc2  9695  rankr1ai  9751  rankuni2b  9806  tcrank  9837  harval2  9950  cfflb  10212  fin23lem20  10290  fin23lem38  10302  isf32lem2  10307  intwun  10688  inttsk  10727  intgru  10767  dfnn2  12199  dfuzi  12625  trclubi  14962  trclubgi  14963  trclub  14964  trclubg  14965  cotrtrclfv  14978  trclun  14980  dfrtrcl2  15028  mremre  17565  isacs1i  17618  mrelatglb  18519  cycsubg  19140  efgrelexlemb  19680  efgcpbllemb  19685  frgpuplem  19702  rgspnmin  20524  primefld  20714  cssmre  21602  toponmre  22980  1stcfb  23332  ptcnplem  23508  fbssfi  23724  uffix  23808  ufildom1  23813  alexsublem  23931  alexsubALTlem4  23937  tmdgsum2  23983  bcth3  25231  limciun  25795  aalioulem3  26242  sltval2  27568  sltres  27574  nocvxminlem  27689  eqscut2  27718  scutun12  27722  scutbdaybnd  27727  scutbdaybnd2  27728  scutbdaylt  27730  madebdaylemlrcut  27810  cofcut1  27828  cofcutr  27832  dfn0s2  28224  shintcli  31258  shsval2i  31316  ococin  31337  chsupsn  31342  elrgspnlem4  33196  fldgensdrg  33264  fldgenssv  33265  fldgenssp  33268  insiga  34127  ldsysgenld  34150  ldgenpisyslem2  34154  mclsssvlem  35549  mclsax  35556  mclsind  35557  untint  35699  dfon2lem8  35778  dfon2lem9  35779  clsint2  36317  topmeet  36352  topjoin  36353  heibor1lem  37803  ismrcd1  42686  mzpincl  42722  mzpf  42724  mzpindd  42734  onintunirab  43216  oninfint  43225  clublem  43599  dftrcl3  43709  brtrclfv2  43716  dfrtrcl3  43722  intsaluni  46327  intsal  46328  salgenss  46334  salgencntex  46341  intubeu  48972