Theorem intss1 4963

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 3484	. . . 4 ⊢ 𝑥 ∈ V
2	1	elint 4952	. . 3 ⊢ (𝑥 ∈ ∩ 𝐵 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦))
3		eleq1 2829	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
4		eleq2 2830	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝐴))
5	3, 4	imbi12d 344	. . . . 5 ⊢ (𝑦 = 𝐴 → ((𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) ↔ (𝐴 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
6	5	spcgv 3596	. . . 4 ⊢ (𝐴 ∈ 𝐵 → (∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) → (𝐴 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
7	6	pm2.43a 54	. . 3 ⊢ (𝐴 ∈ 𝐵 → (∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) → 𝑥 ∈ 𝐴))
8	2, 7	biimtrid 242	. 2 ⊢ (𝐴 ∈ 𝐵 → (𝑥 ∈ ∩ 𝐵 → 𝑥 ∈ 𝐴))
9	8	ssrdv 3989	1 ⊢ (𝐴 ∈ 𝐵 → ∩ 𝐵 ⊆ 𝐴)

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-ss 3968  df-int 4947

This theorem is referenced by:  intminss  4974  intmin3  4976  intab  4978  int0el  4979  trintss  5278  intex  5344  intidg  5462  oneqmini  6436  sorpssint  7753  onint  7810  onssmin  7812  onnmin  7818  nnawordex  8675  cofon1  8710  cofonr  8712  dffi2  9463  inficl  9465  dffi3  9471  tcmin  9781  tc2  9782  rankr1ai  9838  rankuni2b  9893  tcrank  9924  harval2  10037  cfflb  10299  fin23lem20  10377  fin23lem38  10389  isf32lem2  10394  intwun  10775  inttsk  10814  intgru  10854  dfnn2  12279  dfuzi  12709  trclubi  15035  trclubgi  15036  trclub  15037  trclubg  15038  cotrtrclfv  15051  trclun  15053  dfrtrcl2  15101  mremre  17647  isacs1i  17700  mrelatglb  18605  cycsubg  19226  efgrelexlemb  19768  efgcpbllemb  19773  frgpuplem  19790  rgspnmin  20615  primefld  20806  cssmre  21711  toponmre  23101  1stcfb  23453  ptcnplem  23629  fbssfi  23845  uffix  23929  ufildom1  23934  alexsublem  24052  alexsubALTlem4  24058  tmdgsum2  24104  bcth3  25365  limciun  25929  aalioulem3  26376  sltval2  27701  sltres  27707  nocvxminlem  27822  eqscut2  27851  scutun12  27855  scutbdaybnd  27860  scutbdaybnd2  27861  scutbdaylt  27863  madebdaylemlrcut  27937  cofcut1  27954  cofcutr  27958  dfn0s2  28336  shintcli  31348  shsval2i  31406  ococin  31427  chsupsn  31432  elrgspnlem4  33249  fldgensdrg  33316  fldgenssv  33317  fldgenssp  33320  insiga  34138  ldsysgenld  34161  ldgenpisyslem2  34165  mclsssvlem  35567  mclsax  35574  mclsind  35575  untint  35712  dfon2lem8  35791  dfon2lem9  35792  clsint2  36330  topmeet  36365  topjoin  36366  heibor1lem  37816  ismrcd1  42709  mzpincl  42745  mzpf  42747  mzpindd  42757  onintunirab  43239  oninfint  43248  clublem  43623  dftrcl3  43733  brtrclfv2  43740  dfrtrcl3  43746  intsaluni  46344  intsal  46345  salgenss  46351  salgencntex  46358  intubeu  48873