Theorem intss1 4930

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

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

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-ss 3934  df-int 4914

This theorem is referenced by:  intminss  4941  intmin3  4943  intab  4945  int0el  4946  trintss  5236  intex  5302  intidg  5420  oneqmini  6388  sorpssint  7712  onint  7769  onssmin  7771  onnmin  7777  nnawordex  8604  cofon1  8639  cofonr  8641  dffi2  9381  inficl  9383  dffi3  9389  tcmin  9701  tc2  9702  rankr1ai  9758  rankuni2b  9813  tcrank  9844  harval2  9957  cfflb  10219  fin23lem20  10297  fin23lem38  10309  isf32lem2  10314  intwun  10695  inttsk  10734  intgru  10774  dfnn2  12206  dfuzi  12632  trclubi  14969  trclubgi  14970  trclub  14971  trclubg  14972  cotrtrclfv  14985  trclun  14987  dfrtrcl2  15035  mremre  17572  isacs1i  17625  mrelatglb  18526  cycsubg  19147  efgrelexlemb  19687  efgcpbllemb  19692  frgpuplem  19709  rgspnmin  20531  primefld  20721  cssmre  21609  toponmre  22987  1stcfb  23339  ptcnplem  23515  fbssfi  23731  uffix  23815  ufildom1  23820  alexsublem  23938  alexsubALTlem4  23944  tmdgsum2  23990  bcth3  25238  limciun  25802  aalioulem3  26249  sltval2  27575  sltres  27581  nocvxminlem  27696  eqscut2  27725  scutun12  27729  scutbdaybnd  27734  scutbdaybnd2  27735  scutbdaylt  27737  madebdaylemlrcut  27817  cofcut1  27835  cofcutr  27839  dfn0s2  28231  shintcli  31265  shsval2i  31323  ococin  31344  chsupsn  31349  elrgspnlem4  33203  fldgensdrg  33271  fldgenssv  33272  fldgenssp  33275  insiga  34134  ldsysgenld  34157  ldgenpisyslem2  34161  mclsssvlem  35556  mclsax  35563  mclsind  35564  untint  35706  dfon2lem8  35785  dfon2lem9  35786  clsint2  36324  topmeet  36359  topjoin  36360  heibor1lem  37810  ismrcd1  42693  mzpincl  42729  mzpf  42731  mzpindd  42741  onintunirab  43223  oninfint  43232  clublem  43606  dftrcl3  43716  brtrclfv2  43723  dfrtrcl3  43729  intsaluni  46334  intsal  46335  salgenss  46341  salgencntex  46348  intubeu  48976